		Search-engine friendly clone of the ACL2 documentation.

Vl-make-n-bit-div-rem

Vl-make-n-bit-div-core

Core of a division/remainder module.

Signature
(vl-make-n-bit-div-core 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_CORE which implements a basic restoring division algorithm in terms of primitives.

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

Definitions and Theorems

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

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

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

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

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

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