		Search-engine friendly clone of the ACL2 documentation.

Occform

Vl-make-n-bit-mult

Generate an multiplier module.

Signature
(vl-make-n-bit-mult n) → mods
Arguments: 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).

We produce VL_N_BIT_MULT for the given n, which is written using primitives but is semantically equal to:

module VL_N_BIT_MULT (out, a, b) ;
  output [n-1:0] out;
  input [n-1:0] a;
  input [n-1:0] b;
  assign out = a * b;
endmodule

We use a naive, sum-of-partial-products style multiplier. It computes N (shifted) partial products (using N gates apiece), then sums them together with n-1 instances of an N-bit wide adder circuit.

The semantics of Verilog require that if any bit of a or b is X or Z, then every bit of the output is X. We implement this explicitly, which adds a layer of X-detection around the core circuitry.

Definitions and Theorems

Function: vl-make-n-bit-mult

(defun vl-make-n-bit-mult (n)
 (declare (xargs :guard (posp n)))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-make-n-bit-mult))
  (declare (ignorable __function__))
  (b*
   ((n (lposfix n))
    ((when (eql n 1))
     (list *vl-1-bit-mult*
           *vl-1-bit-and* *vl-1-bit-xor*))
    (name (hons-copy (cat "VL_" (natstr n) "_BIT_MULT")))
    ((mv o-expr o-port o-portdecl o-vardecl)
     (vl-occform-mkport "o" :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))
    ((mv p-exprs p-vardecls)
     (vl-occform-mkwires "p" 0 n :width n))
    ((mv s-exprs s-vardecls)
     (vl-occform-mkwires "s" 0 (- n 1)
                         :width n))
    ((mv c-exprs c-vardecls)
     (vl-occform-mkwires "c" 0 (- n 1)
                         :width 1))
    (p-insts (vl-partprod-insts 0 n))
    (adder-mods (vl-make-n-bit-adder-core n))
    (adder-mod (car adder-mods))
    (adders
         (vl-simple-inst-list adder-mod "add" s-exprs c-exprs
                              (cons (car (last p-exprs))
                                    (butlast s-exprs 1))
                              (cdr (rev p-exprs))
                              (replicate (- n 1) |*sized-1'b0*|)))
    (ans (car (last s-exprs)))
    (xprop-modules (vl-make-n-bit-x-propagator n n))
    (xprop-mod (car xprop-modules))
    (xprop-inst (vl-simple-inst xprop-mod
                                "xprop" o-expr ans a-expr b-expr))
    (mod
     (make-vl-module
         :name name
         :origname name
         :ports (list o-port a-port b-port)
         :portdecls (list o-portdecl a-portdecl b-portdecl)
         :vardecls (list* o-vardecl a-vardecl b-vardecl
                          (append p-vardecls s-vardecls c-vardecls))
         :modinsts (append p-insts adders (list xprop-inst))
         :minloc *vl-fakeloc*
         :maxloc *vl-fakeloc*)))
   (list* mod
          (cons *vl-1-bit-buf*
                (append adder-mods xprop-modules))))))

Theorem: vl-modulelist-p-of-vl-make-n-bit-mult

(defthm vl-modulelist-p-of-vl-make-n-bit-mult
  (b* ((mods (vl-make-n-bit-mult n)))
    (vl-modulelist-p mods))
  :rule-classes :rewrite)

Theorem: type-of-vl-make-n-bit-mult

(defthm type-of-vl-make-n-bit-mult
  (and (true-listp (vl-make-n-bit-mult n))
       (consp (vl-make-n-bit-mult n)))
  :rule-classes :type-prescription)

Theorem: vl-make-n-bit-mult-of-pos-fix-n

(defthm vl-make-n-bit-mult-of-pos-fix-n
  (equal (vl-make-n-bit-mult (pos-fix n))
         (vl-make-n-bit-mult n)))

Theorem: vl-make-n-bit-mult-pos-equiv-congruence-on-n

(defthm vl-make-n-bit-mult-pos-equiv-congruence-on-n
  (implies (acl2::pos-equiv n n-equiv)
           (equal (vl-make-n-bit-mult n)
                  (vl-make-n-bit-mult n-equiv)))
  :rule-classes :congruence)