Generate a wide reduction AND, OR, or XOR module.
(vl-make-n-bit-reduction-op type n) → mods
The
module VL_N_BIT_REDUCTION_{AND,OR,XOR} (out, in) ; output out; input [N-1:0] in; // Then, one of: assign out = ∈ // For AND assign out = |in; // For OR assign out = ^in; // For XOR endmodule
For instance, for a 4-bit reduction xor, we actually generate:
wire [2:0] temp; xor(temp0, in1, in0); xor(temp1, in2, temp0); xor(temp2, in3, temp1); xor(out, in4, temp2);
Function:
(defun vl-make-n-bit-reduction-op (type n) (declare (xargs :guard (and (member type (list :vl-unary-bitand :vl-unary-bitor :vl-unary-xor)) (posp n)))) (declare (xargs :guard t)) (let ((__function__ 'vl-make-n-bit-reduction-op)) (declare (ignorable __function__)) (b* ((n (lposfix n)) (name (hons-copy (cat "VL_" (natstr n) "_BIT_REDUCTION_" (case type (:vl-unary-bitand "AND") (:vl-unary-bitor "OR") (otherwise "XOR"))))) ((mv out-expr out-port out-portdecl out-vardecl) (vl-occform-mkport "out" :vl-output 1)) ((mv in-expr in-port in-portdecl in-vardecl) (vl-occform-mkport "in" :vl-input n)) (ports (list out-port in-port)) (portdecls (list out-portdecl in-portdecl)) (prim (case type (:vl-unary-bitand *vl-1-bit-and*) (:vl-unary-bitor *vl-1-bit-or*) (otherwise *vl-1-bit-xor*))) ((when (< n 3)) (b* (((mv inst prim) (if (eql n 1) (mv (vl-simple-inst *vl-1-bit-buf* "ans" out-expr in-expr) *vl-1-bit-buf*) (mv (vl-simple-inst prim "ans" out-expr (vl-make-bitselect in-expr 0) (vl-make-bitselect in-expr 1)) prim)))) (list (make-vl-module :name name :origname name :ports ports :portdecls portdecls :vardecls (list in-vardecl out-vardecl) :modinsts (list inst) :minloc *vl-fakeloc* :maxloc *vl-fakeloc*) prim))) ((mv temp-expr temp-vardecl) (vl-occform-mkwire "temp" (- n 2))) (out-wires (append (vl-make-list-of-bitselects temp-expr 0 (- n 3)) (list out-expr))) (lhs-wires (vl-make-list-of-bitselects in-expr 1 (- n 1))) (rhs-wires (cons (vl-make-bitselect in-expr 0) (vl-make-list-of-bitselects temp-expr 0 (- n 3)))) (insts (vl-simple-inst-list prim "bit" out-wires lhs-wires rhs-wires))) (list (make-vl-module :name name :origname name :ports ports :portdecls portdecls :vardecls (list in-vardecl out-vardecl temp-vardecl) :modinsts insts :minloc *vl-fakeloc* :maxloc *vl-fakeloc*) prim))))
Theorem:
(defthm vl-modulelist-p-of-vl-make-n-bit-reduction-op (b* ((mods (vl-make-n-bit-reduction-op type n))) (vl-modulelist-p mods)) :rule-classes :rewrite)
Theorem:
(defthm type-of-vl-make-n-bit-reduction-op (and (true-listp (vl-make-n-bit-reduction-op type n)) (consp (vl-make-n-bit-reduction-op type n))) :rule-classes :type-prescription)
Theorem:
(defthm vl-make-n-bit-reduction-op-of-pos-fix-n (equal (vl-make-n-bit-reduction-op type (pos-fix n)) (vl-make-n-bit-reduction-op type n)))
Theorem:
(defthm vl-make-n-bit-reduction-op-pos-equiv-congruence-on-n (implies (acl2::pos-equiv n n-equiv) (equal (vl-make-n-bit-reduction-op type n) (vl-make-n-bit-reduction-op type n-equiv))) :rule-classes :congruence)