Generate an unsigned remainder module.
(vl-make-n-bit-unsigned-rem n) → mods
We generate
module VL_N_BIT_UNSIGNED_REM (out, a, b) ; output [n-1:0] out; input [n-1:0] a; input [n-1:0] b; assign out = a % b; endmodule
This is a thin wrapper around vl-make-n-bit-div-rem. It uses a naive N-step restoring division algorithm.
Function:
(defun vl-make-n-bit-unsigned-rem (n) (declare (xargs :guard (posp n))) (declare (xargs :guard t)) (let ((__function__ 'vl-make-n-bit-unsigned-rem)) (declare (ignorable __function__)) (b* ((n (lposfix n)) (name (hons-copy (cat "VL_" (natstr n) "_BIT_UNSIGNED_REM"))) ((mv out-expr out-port out-portdecl out-vardecl) (vl-occform-mkport "out" :vl-output n)) ((mv a-expr a-port a-portdecl a-vardecl) (vl-occform-mkport "a" :vl-input n)) ((mv b-expr b-port b-portdecl b-vardecl) (vl-occform-mkport "b" :vl-input n)) ((mv u-expr u-vardecl) (vl-occform-mkwire "unused" n)) (core-mods (vl-make-n-bit-div-rem n)) (core-mod (car core-mods)) (core-inst (vl-simple-inst core-mod "core" u-expr out-expr a-expr b-expr))) (cons (make-vl-module :name name :origname name :ports (list out-port a-port b-port) :portdecls (list out-portdecl a-portdecl b-portdecl) :vardecls (list out-vardecl a-vardecl b-vardecl u-vardecl) :modinsts (list core-inst) :minloc *vl-fakeloc* :maxloc *vl-fakeloc*) core-mods))))
Theorem:
(defthm vl-modulelist-p-of-vl-make-n-bit-unsigned-rem (b* ((mods (vl-make-n-bit-unsigned-rem n))) (vl-modulelist-p mods)) :rule-classes :rewrite)
Theorem:
(defthm type-of-vl-make-n-bit-unsigned-rem (and (true-listp (vl-make-n-bit-unsigned-rem n)) (consp (vl-make-n-bit-unsigned-rem n))) :rule-classes :type-prescription)
Theorem:
(defthm vl-make-n-bit-unsigned-rem-of-pos-fix-n (equal (vl-make-n-bit-unsigned-rem (pos-fix n)) (vl-make-n-bit-unsigned-rem n)))
Theorem:
(defthm vl-make-n-bit-unsigned-rem-pos-equiv-congruence-on-n (implies (acl2::pos-equiv n n-equiv) (equal (vl-make-n-bit-unsigned-rem n) (vl-make-n-bit-unsigned-rem n-equiv))) :rule-classes :congruence)