• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
        • *vl-1-bit-approx-mux*
        • *vl-1-bit-mux*
        • Nedgeflop
        • Vl-primitive-mkport
        • *vl-1-bit-assign*
        • *vl-1-bit-zmux*
        • Vl-primitive-mkwire
        • *vl-1-bit-bufif1*
        • *vl-1-bit-bufif0*
        • *vl-1-bit-delay-1*
        • *vl-1-bit-ceq*
        • *vl-1-bit-buf*
        • *vl-1-bit-rcmos*
        • *vl-1-bit-latch*
        • *vl-1-bit-cmos*
        • *vl-1-bit-power*
        • *vl-1-bit-rpmos*
        • *vl-1-bit-rnmos*
        • *vl-1-bit-pmos*
        • *vl-1-bit-nmos*
        • *vl-1-bit-ground*
        • *vl-1-bit-tranif1*
        • *vl-1-bit-tranif0*
        • *vl-1-bit-rtranif1*
        • *vl-1-bit-rtranif0*
        • *vl-1-bit-rtran*
        • *vl-1-bit-tran*
        • *vl-1-bit-notif1*
        • *vl-1-bit-notif0*
        • *vl-1-bit-and*
        • *vl-1-bit-xor*
        • *vl-1-bit-xnor*
        • *vl-1-bit-pullup*
        • *vl-1-bit-pulldown*
        • *vl-1-bit-or*
        • *vl-1-bit-not*
        • *vl-1-bit-nor*
        • *vl-1-bit-nand*
        • *vl-1-bit-z*
        • *vl-1-bit-x*
        • *vl-1-bit-t*
        • *vl-1-bit-f*
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • Svl
    • X86isa
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Primitives

*vl-1-bit-tran*

Primitive bidirectional connection.

The Verilog meaning of this module is:

module VL_1_BIT_TRAN (a, b);
  inout a ;
  inout b ;
  tran gate (a, b) ;
endmodule

VL takes this as a primitive. The gate-elim transform converts certain tran gates into instances of this module.

There is no sensible way to model this in ESIM and hence there is no ESIM equivalent. However, this module may be a convenient target for other back-end tools.

Definition: *vl-1-bit-tran*

(defconst *vl-1-bit-tran*
 (b*
  ((name "VL_1_BIT_TRAN")
   (atts '(("VL_PRIMITIVE") ("VL_HANDS_OFF")))
   ((mv a-expr a-port a-portdecl a-vardecl)
    (vl-primitive-mkport "a" :vl-inout))
   ((mv b-expr b-port b-portdecl b-vardecl)
    (vl-primitive-mkport "b" :vl-inout))
   (gate
    (make-vl-gateinst :type :vl-tran
                      :name "gate"
                      :args (list (make-vl-plainarg :expr a-expr
                                                    :dir :vl-inout)
                                  (make-vl-plainarg :expr b-expr
                                                    :dir :vl-inout))
                      :loc *vl-fakeloc*)))
  (hons-copy (make-vl-module :name name
                             :origname name
                             :ports (list a-port b-port)
                             :portdecls (list a-portdecl b-portdecl)
                             :vardecls (list a-vardecl b-vardecl)
                             :gateinsts (list gate)
                             :minloc *vl-fakeloc*
                             :maxloc *vl-fakeloc*
                             :atts atts
                             :esim nil))))