		Search-engine friendly clone of the ACL2 documentation.

Primitives

vl-1-bit-approx-mux

Primitive 1-bit (more conservative) multiplexor module.

The Verilog definition of this module is:

module VL_1_BIT_APPROX_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, and we use it to implement ?: expressions. The corresponding esim primitive is ACL2::*esim-safe-mux*.

The esim semantics are a conservative, inexact approximation of the Verilog semantics, for two reasons.

1. Z Input Handling

In Verilog, the expression sel ? a : b produces a Z value when the selected input is Z. But our corresponding esim primitive produces X in this case.

Occasionally, ?: operators with Z inputs are used in Verilog designs to model efficient muxes, based on tri-state buffers, where the selects are expected to be one-hot. For instance:

assign out = sel1 ? data1 : 1'bz;
assign out = sel2 ? data2 : 1'bz;
assign out = sel3 ? data3 : 1'bz;

Such a circuit could not be modeled correctly using approx-muxes; the esim semantics would always produce an X on the output. To avoid this, VL tries to recognize ?: operators that literally are of the form a ? b : Z, using a simple kind of pattern-matching, and in these cases it uses a different primitive, *vl-1-bit-zmux*, instead of approx muxes.

But in general, the Verilog semantics do not really correspond to any kind of hardware that you would implement. For instance, an AND/OR style mux would always drive its output, regardless of whether its inputs were driven. So the ESIM semantics, which treat the output as X instead of Z in this case, are arguably more realistic and safer than the Verilog semantics.

2. X Select Handling

In Verilog, when sel evaluates to X or Z, the expression sel ? a : b may still produce a good 1 or 0 value when both data inputs a and b share this value.

For certain kinds of mux implementations, this seems overly optimistic, and our esim semantics for an approx mux is that whenever sel is X, we output is X, even if the inputs agree. For more discussion about this issue and the tradeoffs involved, see ACL2::4v-ite.

For special cases where this approximation is not acceptable, VL implements a special VL_X_SELECT that can be used to override this behavior. ?: operators that are annotated with this attribute will be implemented in a less conservative way, as *vl-1-bit-mux* primitives. See vl-mux-occform for more information.

Definition: *vl-1-bit-approx-mux*

(defconst *vl-1-bit-approx-mux*
 (b*
  ((name "VL_1_BIT_APPROX_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-safe-mux*))))