• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • ACL2
  • Macro-libraries
  • 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-mux*

Primitive 1-bit (less conservative) multiplexor module.

The Verilog definition of this module is:

module VL_1_BIT_MUX (out, sel, a, b) ;
  output out;
  input sel;
  input a;
  input b;
  assign out = sel ? a : b;
endmodule

VL takes this as a primitive. The corresponding esim primitive is ACL2::*esim-unsafe-mux*.

Ordinarily, VL will not use this module. Instead, ?: operators will be implemented using either *vl-1-bit-approx-mux* or *vl-1-bit-zmux* modules.

The only reason we have this module at all is that, occasionally, you may find that an approx mux is too conservative. If this causes you problems, you may instruct VL to instead produce a less-conservative *vl-1-bit-mux* by adding a VL_X_SELECT attribute; see vl-mux-occform for more information.

In the ESIM semantics, a *vl-1-bit-mux* is identical to a *vl-1-bit-approx-mux* except in the cases where the select is unknown (X or Z) and the data inputs agree on some good, Boolean value. For instance:

• X ? 1 : 1
• X ? 0 : 0

In these cases, an approx-mux produces X, whereas a non-approx mux will produce the shared value of the data inputs.

This less-conservative behavior may not necessarily be a realistic model of how some physical muxes will operate, and may lead to somewhat slower symbolic simulation performance in certain cases. For additional discussion of these issues, see *vl-1-bit-approx-mux* and ACL2::4v-ite.

Note that, like an approx-mux, a vl-1-bit-mux still produces X when the selected data input is Z.

Definition: *vl-1-bit-mux*

(defconst *vl-1-bit-mux*
 (b*
  ((name "VL_1_BIT_MUX")
   (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))
   ((mv b-expr b-port b-portdecl b-vardecl)
    (vl-primitive-mkport "b" :vl-input))
   (assign
     (make-vl-assign
          :lvalue out-expr
          :expr (make-vl-nonatom :op :vl-qmark
                                 :args (list sel-expr a-expr b-expr)
                                 :finalwidth 1
                                 :finaltype :vl-unsigned)
          :loc *vl-fakeloc*)))
  (hons-copy
       (make-vl-module
            :name name
            :origname name
            :ports (list out-port sel-port a-port b-port)
            :portdecls (list out-portdecl
                             sel-portdecl a-portdecl b-portdecl)
            :vardecls (list out-vardecl
                            sel-vardecl a-vardecl b-vardecl)
            :assigns (list assign)
            :minloc *vl-fakeloc*
            :maxloc *vl-fakeloc*
            :atts atts
            :esim acl2::*esim-unsafe-mux*))))