Generate an N-bit basic ripple-carry adder module.
(vl-make-n-bit-adder-core n) → 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
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.
Function:
(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:
(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:
(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:
(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:
(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)