• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • 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
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Primitives

*vl-1-bit-zmux*

Primitive tri-state buffer module.

The Verilog meaning of this module is:

module VL_1_BIT_ZMUX (out, sel, a);
  output out;
  input sel;
  input a;
  assign out = sel ? a : 1'bZ;
endmodule

VL takes this as a primitive. It is used in vl-mux-occform as the basis for conditional expressions with Z branches that are typically used to implement muxes.

Verilog truth table:

 sel    a    |   out         sel    a        out
-------------+---------     -------------+-----------
  0     0    |    z           x     0    |    x
  0     1    |    z           x     1    |    x
  0     x    |    z           x     x    |    x
  0     z    |    z           x     z    |    x
  1     0    |    0           z     0    |    x
  1     1    |    1           z     1    |    x
  1     x    |    x           z     x    |    x
  1     z    |    z           z     z    |    x

The corresponding esim primitive is ACL2::*esim-tri*, which drives its output to (tristate sel a); see ACL2::4v-tristate. This matches the Verilog truth table exactly.

Definition: *vl-1-bit-zmux*

(defconst *vl-1-bit-zmux*
 (b*
  ((name "VL_1_BIT_ZMUX")
   (atts '(("VL_PRIMITIVE") ("VL_HANDS_OFF")))
   ((mv out-expr
        out-port out-portdecl out-vardecl)
    (vl-primitive-mkport "out" :vl-output))
   ((mv sel-expr
        sel-port sel-portdecl sel-vardecl)
    (vl-primitive-mkport "sel" :vl-input))
   ((mv a-expr a-port a-portdecl a-vardecl)
    (vl-primitive-mkport "a" :vl-input))
   (assign
    (make-vl-assign
        :lvalue out-expr
        :expr
        (make-vl-nonatom :op :vl-qmark
                         :args (list sel-expr a-expr |*sized-1'bz*|)
                         :finalwidth 1
                         :finaltype :vl-unsigned)
        :loc *vl-fakeloc*)))
  (hons-copy
       (make-vl-module
            :name name
            :ports (list out-port sel-port a-port)
            :portdecls (list out-portdecl sel-portdecl a-portdecl)
            :vardecls (list out-vardecl sel-vardecl a-vardecl)
            :assigns (list assign)
            :minloc *vl-fakeloc*
            :maxloc *vl-fakeloc*
            :atts atts
            :origname name
            :esim acl2::*esim-tri*))))