		Search-engine friendly clone of the ACL2 documentation.

Occform

Vl-make-n-bit-mux

Generate a wide multiplexor module.

Signature
(vl-make-n-bit-mux n approxp) → mods
Arguments: n — Guard (posp n).; approxp — Guard (booleanp approxp).
Returns: mods — A non-empty module list. The first module in the list is the desired module; the other modules are any necessary supporting modules.
Type (vl-modulelist-p mods).

We generate a module that is written using gates and which is a conservative approximation of the following:

module VL_N_BIT_MUX (out, sel, a, b);  // or VL_N_BIT_APPROX_MUX
  output [N-1:0] out;
  input sel;
  input [N-1:0] a;
  input [N-1:0] b;

  assign out = sel ? a : b;
endmodule

We generate a "regular" or "approx" versions depending on approxp. Either version is a conservative, inexact approximations of the Verilog semantics of the conditional operator, because we cannot really preserve Zs appropriately using gates. Perhaps the semantics of ?: are not exactly synthesizable?

When approxp is NIL, we try to model Verilog's semantics as closely as possible; in this case X ? 1 : 1 and X ? 0 : 0 produce 1 and 0, respectively. But when approxp is T, we conservatively produce X in these cases, instead.

For some years we implemented both kinds of muxes using gates, roughly as

out[i] = (sel & a[i]) | (~sel & b[i]), for approx muxes, or
out[i] = (sel & a[i]) | (~sel & b[i]) | (a[i] & b[i]) otherwise

But we later (October 2013) realized a bizarre inconsistency in the way that approx-muxes handled things. In particular:

If both a[i] and b[i] are 0, then the approx-mux expression produces a good 0 output (because the AND gates propagate the zero.) However,
If both a[i] and b[i] are 1, then the approx-mux expression produces an X because the AND gates can't optimize things.

Since our general intent is to model arbitrary mux implementations with approx muxes, this optimistic treatment for 0 seems suspicious or incorrect. We ultimately decided to adopt both kinds of muxes as new VL primitives rather than implement them with gates. See *vl-1-bit-approx-mux* and *vl-1-bit-mux* for details.

You might expect that it's better to set approxp to NIL and get the behavior that is closest to Verilog. But the more conservative version may generally produce smaller AIGs since the output doesn't depend upon the inputs when the select is X. So, we generally set approxp to T.

Definitions and Theorems

Function: vl-make-n-bit-mux

(defun vl-make-n-bit-mux (n approxp)
 (declare (xargs :guard (and (posp n) (booleanp approxp))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-make-n-bit-mux))
  (declare (ignorable __function__))
  (b*
   ((n (lposfix n))
    (onebitmux (if approxp *vl-1-bit-approx-mux*
                 *vl-1-bit-mux*))
    ((when (eql n 1)) (list onebitmux))
    (name (cat "VL_" (natstr n)
               "_BIT_"
               (if approxp "APPROX_MUX" "MUX")))
    ((mv out-expr
         out-port out-portdecl out-vardecl)
     (vl-occform-mkport "out" :vl-output n))
    ((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-occform-mkport "a" :vl-input n))
    ((mv b-expr b-port b-portdecl b-vardecl)
     (vl-occform-mkport "b" :vl-input n))
    (out-wires (vl-make-list-of-bitselects out-expr 0 (- n 1)))
    (a-wires (vl-make-list-of-bitselects a-expr 0 (- n 1)))
    (b-wires (vl-make-list-of-bitselects b-expr 0 (- n 1)))
    (insts
         (vl-simple-inst-list onebitmux
                              "bit" out-wires (replicate n sel-expr)
                              a-wires b-wires))
    (mod (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)
              :modinsts insts
              :minloc *vl-fakeloc*
              :maxloc *vl-fakeloc*)))
   (list mod onebitmux))))

Theorem: vl-modulelist-p-of-vl-make-n-bit-mux

(defthm vl-modulelist-p-of-vl-make-n-bit-mux
  (b* ((mods (vl-make-n-bit-mux n approxp)))
    (vl-modulelist-p mods))
  :rule-classes :rewrite)

Theorem: type-of-vl-make-n-bit-mux

(defthm type-of-vl-make-n-bit-mux
  (and (true-listp (vl-make-n-bit-mux n approxp))
       (consp (vl-make-n-bit-mux n approxp)))
  :rule-classes :type-prescription)

Theorem: vl-make-n-bit-mux-of-pos-fix-n

(defthm vl-make-n-bit-mux-of-pos-fix-n
  (equal (vl-make-n-bit-mux (pos-fix n) approxp)
         (vl-make-n-bit-mux n approxp)))

Theorem: vl-make-n-bit-mux-pos-equiv-congruence-on-n

(defthm vl-make-n-bit-mux-pos-equiv-congruence-on-n
  (implies (acl2::pos-equiv n n-equiv)
           (equal (vl-make-n-bit-mux n approxp)
                  (vl-make-n-bit-mux n-equiv approxp)))
  :rule-classes :congruence)

Theorem: vl-make-n-bit-mux-of-bool-fix-approxp

(defthm vl-make-n-bit-mux-of-bool-fix-approxp
  (equal (vl-make-n-bit-mux n (acl2::bool-fix approxp))
         (vl-make-n-bit-mux n approxp)))

Theorem: vl-make-n-bit-mux-iff-congruence-on-approxp

(defthm vl-make-n-bit-mux-iff-congruence-on-approxp
  (implies (iff approxp approxp-equiv)
           (equal (vl-make-n-bit-mux n approxp)
                  (vl-make-n-bit-mux n approxp-equiv)))
  :rule-classes :congruence)