		Search-engine friendly clone of the ACL2 documentation.

Occform

Vl-make-n-bit-reduction-op

Generate a wide reduction AND, OR, or XOR module.

Signature
(vl-make-n-bit-reduction-op type n) → mods
Arguments: type — Guard (member type (list :vl-unary-bitand :vl-unary-bitor :vl-unary-xor)).; 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).

The type must be either :VL-UNARY-BITAND, :VL-UNARY-BITOR, or :VL-UNARY-XOR. We don't deal with nand, nor, or xnor because those should be handled by oprewrite instead. Depending on the type, we generate a module that is written using gates, and which is semantically equivalent to:

module VL_N_BIT_REDUCTION_{AND,OR,XOR} (out, in) ;
  output out;
  input [N-1:0] in;

// Then, one of:

  assign out = &in;     // 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);

Definitions and Theorems

Function: vl-make-n-bit-reduction-op

(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: vl-modulelist-p-of-vl-make-n-bit-reduction-op

(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: type-of-vl-make-n-bit-reduction-op

(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: vl-make-n-bit-reduction-op-of-pos-fix-n

(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: vl-make-n-bit-reduction-op-pos-equiv-congruence-on-n

(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)