Generate an unsigned greater-than or equal comparison module.
(vl-make-n-bit-unsigned-gte n) → mods
We generate a gate-based module that is semantically equivalent to:
module VL_N_BIT_UNSIGNED_GTE (out, a, b) ; output out; input [n-1:0] a; input [n-1:0] b; assign out = a >= b; endmodule
Note that in oprewrite we canonicalize any
The basic idea is to compute
Note that the Verilog semantics require that if
Function:
(defun vl-make-n-bit-unsigned-gte (n) (declare (xargs :guard (posp n))) (declare (xargs :guard t)) (let ((__function__ 'vl-make-n-bit-unsigned-gte)) (declare (ignorable __function__)) (b* ((n (lposfix n)) (name (hons-copy (cat "VL_" (natstr n) "_BIT_UNSIGNED_GTE"))) ((mv out-expr out-port out-portdecl out-vardecl) (vl-primitive-mkport "out" :vl-output)) ((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 bnot-expr bnot-vardecl) (vl-occform-mkwire "bnot" n)) ((mv sum-expr sum-vardecl) (vl-occform-mkwire "sum" n)) ((mv cout-expr cout-vardecl) (vl-primitive-mkwire "cout")) ((cons bnot-mod bnot-support) (vl-make-n-bit-not n)) (bnot-inst (vl-simple-inst bnot-mod "mk_bnot" bnot-expr b-expr)) ((cons core-mod core-support) (vl-make-n-bit-adder-core n)) (core-inst (vl-simple-inst core-mod "core" sum-expr cout-expr a-expr bnot-expr |*sized-1'b1*|)) ((cons xprop-mod xprop-support) (vl-make-n-bit-x-propagator n 1)) (xprop-inst (vl-simple-inst xprop-mod "xprop" out-expr cout-expr a-expr b-expr))) (list* (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 sum-vardecl cout-vardecl bnot-vardecl) :modinsts (list bnot-inst core-inst xprop-inst) :minloc *vl-fakeloc* :maxloc *vl-fakeloc*) bnot-mod core-mod xprop-mod (append bnot-support core-support xprop-support)))))
Theorem:
(defthm vl-modulelist-p-of-vl-make-n-bit-unsigned-gte (b* ((mods (vl-make-n-bit-unsigned-gte n))) (vl-modulelist-p mods)) :rule-classes :rewrite)
Theorem:
(defthm type-of-vl-make-n-bit-unsigned-gte (and (true-listp (vl-make-n-bit-unsigned-gte n)) (consp (vl-make-n-bit-unsigned-gte n))) :rule-classes :type-prescription)
Theorem:
(defthm vl-make-n-bit-unsigned-gte-of-pos-fix-n (equal (vl-make-n-bit-unsigned-gte (pos-fix n)) (vl-make-n-bit-unsigned-gte n)))
Theorem:
(defthm vl-make-n-bit-unsigned-gte-pos-equiv-congruence-on-n (implies (acl2::pos-equiv n n-equiv) (equal (vl-make-n-bit-unsigned-gte n) (vl-make-n-bit-unsigned-gte n-equiv))) :rule-classes :congruence)