		Search-engine friendly clone of the ACL2 documentation.

Occform

Vl-make-n-bit-binary-op

Generate a wide, pointwise AND, OR, XOR, or XNOR module.

Signature
(vl-make-n-bit-binary-op type n) → mods
Arguments: type — Guard (member type '(:vl-and :vl-or :vl-xor :vl-xnor)).; 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-AND, :VL-OR, :VL-XOR, or :VL-XNOR. Depending on the type, we generate a module that is written using primitives but is semantically equivalent to:

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 N is 4 and type is OR, we actually write:

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]);

Definitions and Theorems

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

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

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

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

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

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