Generate a wide, pointwise AND, OR, XOR, or XNOR module.
(vl-make-n-bit-binary-op type n) → mods
The
module VL_N_BIT_POINTWISE_{AND,OR,XOR,XNOR} (out, a, b) ; output [N-1:0] out; input [N-1:0] a; input [N-1:0] b; // Then, one of: assign out = a & b; // for AND assign out = a | b; // for OR assign out = a ^ b; // for XOR assign out = a ~^ b; // for XNOR endmodule
For instance, if
VL_1_BIT_OR bit3 (out[3], a[3], b[3]); VL_1_BIT_OR bit2 (out[2], a[2], b[2]); VL_1_BIT_OR bit1 (out[1], a[1], b[1]); VL_1_BIT_OR bit0 (out[0], a[0], b[0]);
Function:
(defun vl-make-n-bit-binary-op (type n) (declare (xargs :guard (and (member type '(:vl-and :vl-or :vl-xor :vl-xnor)) (posp n)))) (declare (xargs :guard t)) (let ((__function__ 'vl-make-n-bit-binary-op)) (declare (ignorable __function__)) (b* ((n (lposfix n)) (prim (case type (:vl-and *vl-1-bit-and*) (:vl-or *vl-1-bit-or*) (:vl-xor *vl-1-bit-xor*) (otherwise *vl-1-bit-xnor*))) (name (hons-copy (cat "VL_" (natstr n) "_BIT_POINTWISE_" (case type (:vl-and "AND") (:vl-or "OR") (:vl-xor "XOR") (:vl-xnor "XNOR"))))) ((mv out-expr out-port out-portdecl out-vardecl) (vl-occform-mkport "out" :vl-output n)) ((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 prim "bit" out-wires a-wires b-wires))) (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) :modinsts insts :minloc *vl-fakeloc* :maxloc *vl-fakeloc*) prim))))
Theorem:
(defthm vl-modulelist-p-of-vl-make-n-bit-binary-op (b* ((mods (vl-make-n-bit-binary-op type n))) (vl-modulelist-p mods)) :rule-classes :rewrite)
Theorem:
(defthm type-of-vl-make-n-bit-binary-op (and (true-listp (vl-make-n-bit-binary-op type n)) (consp (vl-make-n-bit-binary-op type n))) :rule-classes :type-prescription)
Theorem:
(defthm vl-make-n-bit-binary-op-of-pos-fix-n (equal (vl-make-n-bit-binary-op type (pos-fix n)) (vl-make-n-bit-binary-op type n)))
Theorem:
(defthm vl-make-n-bit-binary-op-pos-equiv-congruence-on-n (implies (acl2::pos-equiv n n-equiv) (equal (vl-make-n-bit-binary-op type n) (vl-make-n-bit-binary-op type n-equiv))) :rule-classes :congruence)