Top-level division/remainder module.
(vl-make-n-bit-div-rem n) → mods
We generate the module
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.
Function:
(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:
(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:
(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:
(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:
(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)