Generate a wide X module.
(vl-make-n-bit-x n) → mods
We generate a module that is semantically equal to:
module VL_N_BIT_ASSIGN (out, in) ; output [n-1:0] out; input [n-1:0] in; assign out = {n{1'bx}}; endmodule
We actually implement these modules using a list of *vl-1-bit-assign* instances, one for each bit. For instance, we implement our four-bit X generator like this:
module VL_4_BIT_X (out, in); output [3:0] out ; input [3:0] in ; wire xwire; VL_1_BIT_X xdriver (xwire); VL_1_BIT_ASSIGN bit_0 (out[0], xwire); VL_1_BIT_ASSIGN bit_1 (out[1], xwire) ; VL_1_BIT_ASSIGN bit_2 (out[2], xwire) ; VL_1_BIT_ASSIGN bit_3 (out[3], xwire) ; endmodule
Function:
(defun vl-make-n-bit-x (n) (declare (xargs :guard (posp n))) (declare (xargs :guard t)) (let ((__function__ 'vl-make-n-bit-x)) (declare (ignorable __function__)) (b* ((n (lposfix n)) ((when (eql n 1)) (list *vl-1-bit-x*)) (name (hons-copy (cat "VL_" (natstr n) "_BIT_X"))) ((mv out-expr out-port out-portdecl out-vardecl) (vl-occform-mkport "out" :vl-output n)) ((mv x-expr x-vardecl) (vl-occform-mkwire "xwire" 1)) (x-inst (vl-simple-inst *vl-1-bit-x* "xdriver" x-expr)) (out-wires (vl-make-list-of-bitselects out-expr 0 (- n 1))) (in-wires (replicate n x-expr)) (out-insts (vl-simple-inst-list *vl-1-bit-assign* "bit" out-wires in-wires))) (list (make-vl-module :name name :origname name :ports (list out-port) :portdecls (list out-portdecl) :vardecls (list out-vardecl x-vardecl) :modinsts (cons x-inst out-insts) :minloc *vl-fakeloc* :maxloc *vl-fakeloc*) *vl-1-bit-assign* *vl-1-bit-x*))))
Theorem:
(defthm vl-modulelist-p-of-vl-make-n-bit-x (b* ((mods (vl-make-n-bit-x n))) (vl-modulelist-p mods)) :rule-classes :rewrite)
Theorem:
(defthm type-of-vl-make-n-bit-x (and (true-listp (vl-make-n-bit-x n)) (consp (vl-make-n-bit-x n))) :rule-classes :type-prescription)
Theorem:
(defthm vl-make-n-bit-x-of-pos-fix-n (equal (vl-make-n-bit-x (pos-fix n)) (vl-make-n-bit-x n)))
Theorem:
(defthm vl-make-n-bit-x-pos-equiv-congruence-on-n (implies (acl2::pos-equiv n n-equiv) (equal (vl-make-n-bit-x n) (vl-make-n-bit-x n-equiv))) :rule-classes :congruence)