		Search-engine friendly clone of the ACL2 documentation.

Occform

Vl-make-n-bit-div-rem

Top-level division/remainder module.

Signature
(vl-make-n-bit-div-rem n) → mods
Arguments: n — Guard (posp 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_REM which exactly implements the Verilog semantics for division and remainder using primitives.

The actual division is carried out by a core module; see vl-make-n-bit-div-core. But this core doesn't properly handle the cases where the divisor is zero, or when there is an X/Z value on either the dividend or the divisor. In these cases, the Verilog semantics say that the entire result must be X.

This module just wraps up the core module with zero- and x-detection circuitry to achieve the desired behavior.

Definitions and Theorems

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

(defun vl-make-n-bit-div-rem (n)
 (declare (xargs :guard (posp n)))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-make-n-bit-div-rem))
  (declare (ignorable __function__))
  (b*
   ((n (lposfix n))
    ((when (eql n 1))
     (list *vl-1-bit-div-rem* *vl-1-bit-x*
           *vl-1-bit-not* *vl-1-bit-and*
           *vl-1-bit-or* *vl-1-bit-xor*))
    (name (hons-copy (cat "VL_" (natstr n) "_BIT_DIV_REM")))
    ((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))
    ((mv qm-expr qm-vardecl)
     (vl-occform-mkwire "qmain" n))
    ((mv rm-expr rm-vardecl)
     (vl-occform-mkwire "rmain" n))
    (core-mods (vl-make-n-bit-div-core n))
    (core-mod (car core-mods))
    (core-inst
         (vl-simple-inst core-mod
                         "core" qm-expr rm-expr e-expr d-expr))
    ((mv nz-expr nz-vardecl)
     (vl-occform-mkwire "nonzero" 1))
    (nz-mods (vl-make-n-bit-reduction-op :vl-unary-bitor n))
    (nz-mod (car nz-mods))
    (nz-inst (vl-simple-inst nz-mod "check0" nz-expr d-expr))
    ((mv x-expr x-vardecl)
     (vl-occform-mkwire "xwire" n))
    ((mv qf-expr qf-vardecl)
     (vl-occform-mkwire "qfix" n))
    ((mv rf-expr rf-vardecl)
     (vl-occform-mkwire "rfix" n))
    (x-mods (vl-make-n-bit-x n))
    (x-mod (car x-mods))
    (x-inst (vl-simple-inst x-mod "xdriver" x-expr))
    (mux-mods (vl-make-n-bit-mux n t))
    (mux-mod (car mux-mods))
    (qf-inst (vl-simple-inst mux-mod "q_zero_fix"
                             qf-expr nz-expr qm-expr x-expr))
    (rf-inst (vl-simple-inst mux-mod "r_zero_fix"
                             rf-expr nz-expr rm-expr x-expr))
    (xprop-mods (vl-make-n-bit-x-propagator n n))
    (xprop-mod (car xprop-mods))
    (q-inst (vl-simple-inst xprop-mod
                            "xdet_q" q-expr qf-expr e-expr d-expr))
    (r-inst (vl-simple-inst xprop-mod
                            "xdet_r" r-expr rf-expr e-expr d-expr)))
   (cons
        (make-vl-module
             :name name
             :origname name
             :ports (list q-port r-port e-port d-port)
             :portdecls (list q-portdecl
                              r-portdecl e-portdecl d-portdecl)
             :vardecls (list q-vardecl r-vardecl e-vardecl d-vardecl
                             qm-vardecl rm-vardecl nz-vardecl
                             x-vardecl qf-vardecl rf-vardecl)
             :modinsts (list core-inst nz-inst
                             x-inst qf-inst rf-inst q-inst r-inst)
             :minloc *vl-fakeloc*
             :maxloc *vl-fakeloc*)
        (append x-mods xprop-mods
                mux-mods nz-mods core-mods)))))

Theorem: vl-modulelist-p-of-vl-make-n-bit-div-rem

(defthm vl-modulelist-p-of-vl-make-n-bit-div-rem
  (b* ((mods (vl-make-n-bit-div-rem n)))
    (vl-modulelist-p mods))
  :rule-classes :rewrite)

Theorem: type-of-vl-make-n-bit-div-rem

(defthm type-of-vl-make-n-bit-div-rem
  (and (true-listp (vl-make-n-bit-div-rem n))
       (consp (vl-make-n-bit-div-rem n)))
  :rule-classes :type-prescription)

Theorem: vl-make-n-bit-div-rem-of-pos-fix-n

(defthm vl-make-n-bit-div-rem-of-pos-fix-n
  (equal (vl-make-n-bit-div-rem (pos-fix n))
         (vl-make-n-bit-div-rem n)))

Theorem: vl-make-n-bit-div-rem-pos-equiv-congruence-on-n

(defthm vl-make-n-bit-div-rem-pos-equiv-congruence-on-n
  (implies (acl2::pos-equiv n n-equiv)
           (equal (vl-make-n-bit-div-rem n)
                  (vl-make-n-bit-div-rem n-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-make-n-bit-div-step: Single step in a basic division/remainder algorithm.
Vl-make-n-bit-div-core: Core of a division/remainder module.