Generate a wide case-equality module.
(vl-make-n-bit-ceq n) → mods
We generate a module that is written using gates and which is semantically equivalent to:
module VL_N_BIT_CEQ (out, a, b) ; output out; input [N-1:0] a; input [N-1:0] b; assign out = (a === b); endmodule
We basically just instantiate *vl-1-bit-ceq* N times and then reduction-and the results.
Function:
(defun vl-make-n-bit-ceq (n) (declare (xargs :guard (posp n))) (declare (xargs :guard t)) (let ((__function__ 'vl-make-n-bit-ceq)) (declare (ignorable __function__)) (b* ((n (lposfix n)) ((when (eql n 1)) (list *vl-1-bit-ceq*)) (name (hons-copy (cat "VL_" (natstr n) "_BIT_CEQ"))) ((mv out-expr out-port out-portdecl out-vardecl) (vl-occform-mkport "out" :vl-output 1)) ((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)) ((mv tmp-expr tmp-vardecl) (vl-occform-mkwire "tmp" n)) (tmp-wires (vl-make-list-of-bitselects tmp-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 *vl-1-bit-ceq* "bit" tmp-wires a-wires b-wires)) (and-mods (vl-make-n-bit-reduction-op :vl-unary-bitand n)) (and-mod (car and-mods)) (and-inst (vl-simple-inst and-mod "mk_out" out-expr tmp-expr))) (list* (make-vl-module :name name :origname name :ports (list out-port a-port b-port) :portdecls (list out-portdecl a-portdecl b-portdecl) :vardecls (list out-vardecl a-vardecl b-vardecl tmp-vardecl) :modinsts (append insts (list and-inst)) :minloc *vl-fakeloc* :maxloc *vl-fakeloc*) *vl-1-bit-ceq* and-mods))))
Theorem:
(defthm vl-modulelist-p-of-vl-make-n-bit-ceq (b* ((mods (vl-make-n-bit-ceq n))) (vl-modulelist-p mods)) :rule-classes :rewrite)
Theorem:
(defthm type-of-vl-make-n-bit-ceq (and (true-listp (vl-make-n-bit-ceq n)) (consp (vl-make-n-bit-ceq n))) :rule-classes :type-prescription)
Theorem:
(defthm vl-make-n-bit-ceq-of-pos-fix-n (equal (vl-make-n-bit-ceq (pos-fix n)) (vl-make-n-bit-ceq n)))
Theorem:
(defthm vl-make-n-bit-ceq-pos-equiv-congruence-on-n (implies (acl2::pos-equiv n n-equiv) (equal (vl-make-n-bit-ceq n) (vl-make-n-bit-ceq n-equiv))) :rule-classes :congruence)