		Search-engine friendly clone of the ACL2 documentation.

Occform

Vl-make-n-bit-zmux

Generate a wide tri-state buffer module.

Signature
(vl-make-n-bit-zmux n) → mods
Arguments: n — Guard (posp n).
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 using *vl-1-bit-zmux* primitives that is semantically equivalent to:

module VL_N_BIT_ZMUX (out, sel, a);
  output [n-1:0] out;
  input sel;
  input [n-1:0] a;
  assign out = sel ? a : n'bz;
endmodule

BOZO is it really equivalent? It seems like it might be conservative.

These modules are used to implement conditional (a.k.a. the ?: or ternary) operators whose last argument is Z. Note that in oprewrite, we canonicalize sel ? Z : a to ~sel ? a : Z, so this actually handles both cases.

Definitions and Theorems

Function: vl-make-n-bit-zmux

(defun vl-make-n-bit-zmux (n)
 (declare (xargs :guard (posp n)))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-make-n-bit-zmux))
  (declare (ignorable __function__))
  (b*
   ((n (lposfix n))
    ((when (eql n 1))
     (list *vl-1-bit-zmux*))
    (name (hons-copy (cat "VL_" (natstr n) "_BIT_ZMUX")))
    ((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))
    (out-wires (vl-make-list-of-bitselects out-expr 0 (- n 1)))
    (a-wires (vl-make-list-of-bitselects a-expr 0 (- n 1)))
    (insts
         (vl-simple-inst-list *vl-1-bit-zmux*
                              "bit" out-wires (replicate n sel-expr)
                              a-wires))
    (mod (make-vl-module
              :name name
              :origname 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)
              :modinsts insts
              :minloc *vl-fakeloc*
              :maxloc *vl-fakeloc*)))
   (list mod *vl-1-bit-zmux*))))

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

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

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

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

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

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

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

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