		Search-engine friendly clone of the ACL2 documentation.

Vl-make-n-bit-div-rem

Vl-make-n-bit-div-step

Single step in a basic division/remainder algorithm.

Signature
(vl-make-n-bit-div-step n) → mods
Arguments: n — Guard (natp 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 the module VL_N_BIT_DIV_STEP in terms of primitives. This module carries out a single step in a simple restoring division algorithm.

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:

Shift the whole register AQ left by 1, then
Modify A and the bottom bit of Q, i.e., Q[0].

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 divisor <= A, we reduce A by the divisor and set the low bit of Q to 1. Otherwise, we leave A alone and set the low bit of Q to 0.

How does VL_N_BIT_DIV_STEP fit into this? It computes the next value of AQ, given the current value of AQ and the divisor. For example, in the 5-bit case, the general idea is something like this:

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:

We do the comparison and subtraction using the same adder core.
We expect the divisor to be given to us already negated, instead of separately negating it in each step.

Note that the semantics of Verilog require that if any bit of the dividend or divisor is X or Z, then every bit of the output is X. We do not deal with this requirement in the individual steps; it's part of the wrapper.

Definitions and Theorems

Function: vl-make-n-bit-div-step

(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: vl-modulelist-p-of-vl-make-n-bit-div-step

(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: type-of-vl-make-n-bit-div-step

(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: vl-make-n-bit-div-step-of-nfix-n

(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: vl-make-n-bit-div-step-nat-equiv-congruence-on-n

(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)