		Search-engine friendly clone of the ACL2 documentation.

Occform

Vl-make-n-bit-signed-gte

Generate a signed greater-than or equal comparison module.

Signature
(vl-make-n-bit-signed-gte 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 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:

A positive, B positive: unsigned comparison of a >= b
A positive, B negative: 1 since positives > negatives
A negative, B positive: 0 since negatives < positives
A negative, B negative: unsigned comparison of a >= b

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.

Definitions and Theorems

Function: vl-make-n-bit-signed-gte

(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: vl-modulelist-p-of-vl-make-n-bit-signed-gte

(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: type-of-vl-make-n-bit-signed-gte

(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: vl-make-n-bit-signed-gte-of-pos-fix-n

(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: vl-make-n-bit-signed-gte-pos-equiv-congruence-on-n

(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)