		Search-engine friendly clone of the ACL2 documentation.

Occform

Vl-make-n-bit-adder-core

Generate an N-bit basic ripple-carry adder module.

Signature
(vl-make-n-bit-adder-core 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 generate a gate-based module with the following interface:

module VL_N_BIT_ADDER_CORE (sum, cout, a, b, cin);
  output [n-1:0] sum;
  output cout;
  input [n-1:0] a;
  input [n-1:0] b;
  input cin;
  ...
endmodule

This is a basic ripple-carry adder formed by chaining together several full-adders; see *vl-1-bit-adder-core*.

This module does NOT correspond to a full addition in Verilog. It computes something akin to assign {cout, sum} = a + b + cin, but it does not handle X's like Verilog does. See vl-make-n-bit-plusminus for the full addition and subtraction modules.

We could probably make a leaner module by using a half-adder for the first bit (which does not have a carry-in) and by dropping the wires on the carry for the last bit, but we think it's best to keep things simple.

Definitions and Theorems

Function: vl-make-n-bit-adder-core

(defun vl-make-n-bit-adder-core (n)
 (declare (xargs :guard (posp n)))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-make-n-bit-adder-core))
  (declare (ignorable __function__))
  (b*
   ((n (lposfix n))
    ((when (eql n 1))
     (cons *vl-1-bit-adder-core*
           *vl-1-bit-adder-core-support*))
    (name (hons-copy (cat "VL_" (natstr n)
                          "_BIT_ADDER_CORE")))
    ((mv sum-expr
         sum-port sum-portdecl sum-vardecl)
     (vl-occform-mkport "sum" :vl-output n))
    ((mv cout-expr
         cout-port cout-portdecl cout-vardecl)
     (vl-primitive-mkport "cout" :vl-output))
    ((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 cin-expr
         cin-port cin-portdecl cin-vardecl)
     (vl-primitive-mkport "cin" :vl-input))
    ((mv carry-expr carry-vardecl)
     (vl-occform-mkwire "carry" (- n 1)))
    (sum-wires (vl-make-list-of-bitselects sum-expr 0 (- n 1)))
    (carry-wires (vl-make-list-of-bitselects carry-expr 0 (- n 2)))
    (a-wires (vl-make-list-of-bitselects a-expr 0 (- n 1)))
    (b-wires (vl-make-list-of-bitselects b-expr 0 (- n 1)))
    (fa-insts
         (vl-simple-inst-list *vl-1-bit-adder-core* "fa_" sum-wires
                              (append carry-wires (list cout-expr))
                              a-wires
                              b-wires (cons cin-expr carry-wires))))
   (list* (make-vl-module
               :name name
               :origname name
               :ports (list sum-port
                            cout-port a-port b-port cin-port)
               :portdecls (list sum-portdecl cout-portdecl
                                a-portdecl b-portdecl cin-portdecl)
               :vardecls (list sum-vardecl cout-vardecl a-vardecl
                               b-vardecl cin-vardecl carry-vardecl)
               :modinsts fa-insts
               :minloc *vl-fakeloc*
               :maxloc *vl-fakeloc*)
          *vl-1-bit-adder-core*
          *vl-1-bit-adder-core-support*))))

Theorem: vl-modulelist-p-of-vl-make-n-bit-adder-core

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

Theorem: type-of-vl-make-n-bit-adder-core

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

Theorem: vl-make-n-bit-adder-core-of-pos-fix-n

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

Theorem: vl-make-n-bit-adder-core-pos-equiv-congruence-on-n

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