Core of a division/remainder module.
(vl-make-n-bit-div-core n) → mods
We generate the module
The core modules we produce here do not properly handle zero divides or detect X/Z values on the dividend and divisor. To see how we correct for these cases, see vl-make-n-bit-div-rem.
Aside from these special cases, the core module does produce the right answer by chaining together N division steps; for details about these steps and for an overview of the algorithm, see vl-make-n-bit-div-step.
As an example, here's what we generate in the four-bit case:
module VL_4_BIT_DIV_CORE (quotient, remainder, dividend, divisor); output [3:0] quotient; output [3:0] remainder; input [3:0] dividend; input [3:0] divisor; wire [3:0] a1, a2, a3; wire [3:0] q1, q2, q3; wire [3:0] divisor_bar; VL_4_BIT_NOT divbar (divisor_bar, divisor); VL_4_BIT_DIV_STEP step0 (a1, q1, 4'b0, dividend, divisor_bar); VL_4_BIT_DIV_STEP step1 (a2, q2, a1, q1, divisor_bar); VL_4_BIT_DIV_STEP step2 (a3, q3, a2, q2, divisor_bar); VL_4_BIT_DIV_STEP step3 (remainder, quotient, a3, q3, divisor_bar); endmodule
Function:
(defun vl-make-n-bit-div-core (n) (declare (xargs :guard (natp n))) (declare (xargs :guard (>= n 2))) (let ((__function__ 'vl-make-n-bit-div-core)) (declare (ignorable __function__)) (b* ((n (lnfix n)) (name (hons-copy (cat "VL_" (natstr n) "_BIT_DIV_CORE"))) ((mv q-expr q-port q-portdecl q-vardecl) (vl-occform-mkport "quotient" :vl-output n)) ((mv r-expr r-port r-portdecl r-vardecl) (vl-occform-mkport "remainder" :vl-output n)) ((mv e-expr e-port e-portdecl e-vardecl) (vl-occform-mkport "dividend" :vl-input n)) ((mv d-expr d-port d-portdecl d-vardecl) (vl-occform-mkport "divisor" :vl-input n)) (neg-mods (vl-make-n-bit-not n)) (step-mods (vl-make-n-bit-div-step n)) (neg-mod (car neg-mods)) (step-mod (car step-mods)) (support (append neg-mods step-mods)) ((mv d~-expr d~-vardecl) (vl-occform-mkwire "divisor_bar" n)) (d~-inst (vl-simple-inst neg-mod "divbar" d~-expr d-expr)) ((mv a-exprs a-vardecls) (vl-occform-mkwires "a" 1 n :width n)) ((mv q-exprs q-vardecls) (vl-occform-mkwires "q" 1 n :width n)) (|n'b0| (make-vl-atom :guts (make-vl-constint :value 0 :origwidth n :origtype :vl-unsigned) :finalwidth n :finaltype :vl-unsigned)) (steps (vl-simple-inst-list step-mod "step" (append a-exprs (list r-expr)) (append q-exprs (list q-expr)) (cons |n'b0| a-exprs) (cons e-expr q-exprs) (replicate n d~-expr)))) (cons (make-vl-module :name name :origname name :portdecls (list q-portdecl r-portdecl e-portdecl d-portdecl) :ports (list q-port r-port e-port d-port) :vardecls (list* q-vardecl r-vardecl e-vardecl d-vardecl d~-vardecl (append a-vardecls q-vardecls)) :modinsts (cons d~-inst steps) :minloc *vl-fakeloc* :maxloc *vl-fakeloc*) support))))
Theorem:
(defthm vl-modulelist-p-of-vl-make-n-bit-div-core (b* ((mods (vl-make-n-bit-div-core n))) (vl-modulelist-p mods)) :rule-classes :rewrite)
Theorem:
(defthm type-of-vl-make-n-bit-div-core (and (true-listp (vl-make-n-bit-div-core n)) (consp (vl-make-n-bit-div-core n))) :rule-classes :type-prescription)
Theorem:
(defthm vl-make-n-bit-div-core-of-nfix-n (equal (vl-make-n-bit-div-core (nfix n)) (vl-make-n-bit-div-core n)))
Theorem:
(defthm vl-make-n-bit-div-core-nat-equiv-congruence-on-n (implies (acl2::nat-equiv n n-equiv) (equal (vl-make-n-bit-div-core n) (vl-make-n-bit-div-core n-equiv))) :rule-classes :congruence)