Single step in a basic division/remainder algorithm.
(vl-make-n-bit-div-step n) → mods
We generate the module
To understand this code you will need to understand restoring division. We sketch our implementation here, but to understand why it works you should see a textbook on computer arithmetic.
Imagine a double-wide register, sometimes called AQ, whose halves we will treat independently as A and Q.
+--------------+--------------+ | 'A' half | 'Q' half | 2n bits total +--------------+--------------+ n bits n bits
Initially, A is zeroed and Q is set to the dividend. Then we take N steps (described below). After these steps, A will contain the remainder and Q will contain the quotient.
In each step, we are going to:
Note that, except for the shifting step, we don't touch Q besides its bottom bit. Since Q eventually becomes the quotient, what we're really doing here is computing the quotient one bit at a time. During the first iteration, we compute its most significant bit. During the next iteration, we compute its next most significant bit, and so on.
The details of each step are as follows. After shifting AQ, we compare the
divisor (which remains fixed throughout all iterations) against A. If the
divisor "fits" into A, i.e., when
How does
module VL_5_BIT_DIV_STEP (a_next, q_next, // Updated AQ a_prev, q_prev, // Starting AQ divisor) ; output [4:0] a_next, q_next; input [4:0] a_prev, q_prev; input [4:0] divisor; // Temporary AQ is the starting AQ, shifted left by 1, // which drops the top bit of A: wire [4:0] a, q; assign {a, q} = {a_prev[3:0], q_prev, 1'b0}; wire fits = divisor <= a; // Does it fit? assign a_next = fits ? a - divisor : a; // Maybe Adjust A assign q_next = {q[3:1], fits}; // Install Q[0] endmodule
The only twists are the following, basic optimizations:
Note that the semantics of Verilog require that if any bit of the dividend
or divisor is
Function:
(defun vl-make-n-bit-div-step (n) (declare (xargs :guard (natp n))) (declare (xargs :guard (>= n 2))) (let ((__function__ 'vl-make-n-bit-div-step)) (declare (ignorable __function__)) (b* ((n (lnfix n)) (name (hons-copy (cat "VL_" (natstr n) "_BIT_DIV_STEP"))) ((mv an-expr an-port an-portdecl an-vardecl) (vl-occform-mkport "a_next" :vl-output n)) ((mv qn-expr qn-port qn-portdecl qn-vardecl) (vl-occform-mkport "q_next" :vl-output n)) ((mv ap-expr ap-port ap-portdecl ap-vardecl) (vl-occform-mkport "a_prev" :vl-input n)) ((mv qp-expr qp-port qp-portdecl qp-vardecl) (vl-occform-mkport "q_prev" :vl-input n)) ((mv d~-expr d~-port d~-portdecl d~-vardecl) (vl-occform-mkport "divisor_bar" :vl-input n)) ((mv a-expr a-vardecl) (vl-occform-mkwire "a" n)) ((mv diff-expr diff-vardecl) (vl-occform-mkwire "diff" n)) ((mv fits-expr fits-vardecl) (vl-occform-mkwire "fits" 1)) (ass-mods (vl-make-n-bit-assign n)) (add-mods (vl-make-n-bit-adder-core n)) (mux-mods (vl-make-n-bit-mux n t)) (support (append ass-mods add-mods mux-mods)) (ass-mod (car ass-mods)) (add-mod (car add-mods)) (mux-mod (car mux-mods)) (init-inst (vl-simple-inst ass-mod "init" a-expr (make-vl-nonatom :op :vl-concat :args (list (vl-make-partselect ap-expr (- n 2) 0) (vl-make-bitselect qp-expr (- n 1))) :finalwidth n :finaltype :vl-unsigned))) (core-inst (vl-simple-inst add-mod "core" diff-expr fits-expr a-expr d~-expr |*sized-1'b1*|)) (amux-inst (vl-simple-inst mux-mod "amux" an-expr fits-expr diff-expr a-expr)) (qout-inst (vl-simple-inst ass-mod "qout" qn-expr (make-vl-nonatom :op :vl-concat :args (list (vl-make-partselect qp-expr (- n 2) 0) fits-expr) :finalwidth n :finaltype :vl-unsigned)))) (cons (make-vl-module :name name :origname name :ports (list an-port qn-port ap-port qp-port d~-port) :portdecls (list an-portdecl qn-portdecl ap-portdecl qp-portdecl d~-portdecl) :vardecls (list an-vardecl qn-vardecl ap-vardecl qp-vardecl d~-vardecl a-vardecl diff-vardecl fits-vardecl) :modinsts (list init-inst core-inst amux-inst qout-inst) :minloc *vl-fakeloc* :maxloc *vl-fakeloc*) support))))
Theorem:
(defthm vl-modulelist-p-of-vl-make-n-bit-div-step (b* ((mods (vl-make-n-bit-div-step n))) (vl-modulelist-p mods)) :rule-classes :rewrite)
Theorem:
(defthm type-of-vl-make-n-bit-div-step (and (true-listp (vl-make-n-bit-div-step n)) (consp (vl-make-n-bit-div-step n))) :rule-classes :type-prescription)
Theorem:
(defthm vl-make-n-bit-div-step-of-nfix-n (equal (vl-make-n-bit-div-step (nfix n)) (vl-make-n-bit-div-step n)))
Theorem:
(defthm vl-make-n-bit-div-step-nat-equiv-congruence-on-n (implies (acl2::nat-equiv n n-equiv) (equal (vl-make-n-bit-div-step n) (vl-make-n-bit-div-step n-equiv))) :rule-classes :congruence)