Generate a signed greater-than or equal comparison module.
(vl-make-n-bit-signed-gte n) → mods
We generate a gate-based module that is semantically equivalent to:
module VL_N_BIT_SIGNED_GTE (out, a, b) ; output out; input signed [n-1:0] a; input signed [n-1:0] b; assign out = a >= b; endmodule
We just do the stupidest thing possible and do cases on the sign bit:
The middle two cases would ordinarily fool an unsigned comparison, e.g., if A is positive and B is negative, then their leading bits are 0 and 1, respectively, so B "looks bigger" even though A is actually bigger. But ordinary unsigned comparisons work in the other cases.
Function:
(defun vl-make-n-bit-signed-gte (n) (declare (xargs :guard (posp n))) (declare (xargs :guard t)) (let ((__function__ 'vl-make-n-bit-signed-gte)) (declare (ignorable __function__)) (b* ((n (lposfix n)) ((when (eql n 1)) (list *vl-1-bit-signed-gte*)) (name (hons-copy (cat "VL_" (natstr n) "_BIT_SIGNED_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 sdiff-expr sdiff-vardecl) (vl-primitive-mkwire "signs_differ")) ((mv adiff-expr adiff-vardecl) (vl-primitive-mkwire "ans_differ")) ((mv asame-expr asame-vardecl) (vl-primitive-mkwire "ans_same")) ((mv main-expr main-vardecl) (vl-primitive-mkwire "main")) (a-msb (vl-make-bitselect a-expr (- n 1))) (b-msb (vl-make-bitselect b-expr (- n 1))) (a-tail (vl-make-partselect a-expr (- n 2) 0)) (b-tail (vl-make-partselect b-expr (- n 2) 0)) (sdiff-inst (vl-simple-inst *vl-1-bit-xor* "mk_sdiff" sdiff-expr a-msb b-msb)) (adiff-inst (vl-simple-inst *vl-1-bit-not* "mk_adiff" adiff-expr a-msb)) ((cons ucmp-mod ucmp-support) (vl-make-n-bit-unsigned-gte (- n 1))) (ucmp-inst (vl-simple-inst ucmp-mod "core" asame-expr a-tail b-tail)) ((cons mux-mod mux-support) (vl-make-n-bit-mux 1 t)) (mux-inst (vl-simple-inst mux-mod "mux" main-expr sdiff-expr adiff-expr asame-expr)) ((cons xprop-mod xprop-support) (vl-make-n-bit-x-propagator n 1)) (xprop-inst (vl-simple-inst xprop-mod "xprop" out-expr main-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 sdiff-vardecl adiff-vardecl asame-vardecl main-vardecl) :modinsts (list sdiff-inst adiff-inst ucmp-inst mux-inst xprop-inst) :minloc *vl-fakeloc* :maxloc *vl-fakeloc*) ucmp-mod mux-mod xprop-mod (append mux-support xprop-support ucmp-support)))))
Theorem:
(defthm vl-modulelist-p-of-vl-make-n-bit-signed-gte (b* ((mods (vl-make-n-bit-signed-gte n))) (vl-modulelist-p mods)) :rule-classes :rewrite)
Theorem:
(defthm type-of-vl-make-n-bit-signed-gte (and (true-listp (vl-make-n-bit-signed-gte n)) (consp (vl-make-n-bit-signed-gte n))) :rule-classes :type-prescription)
Theorem:
(defthm vl-make-n-bit-signed-gte-of-pos-fix-n (equal (vl-make-n-bit-signed-gte (pos-fix n)) (vl-make-n-bit-signed-gte n)))
Theorem:
(defthm vl-make-n-bit-signed-gte-pos-equiv-congruence-on-n (implies (acl2::pos-equiv n n-equiv) (equal (vl-make-n-bit-signed-gte n) (vl-make-n-bit-signed-gte n-equiv))) :rule-classes :congruence)