		Search-engine friendly clone of the ACL2 documentation.

Occform

Vl-make-n-bit-unsigned-gte

Generate an unsigned greater-than or equal comparison module.

Signature
(vl-make-n-bit-unsigned-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_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 <, <=, and > operators into the >= form, so this module actually handles all inequality comparisons.

The basic idea is to compute a + ~b + 1 and look at the carry chain. We do this by directly instantiating an adder. This might be somewhat inefficient since we really don't need to be computing the sum. On the other hand, there are really not very many comparison operators so we suspect we do not need to be particularly efficient, and hopefully in any AIG or S-Expression based representations the extra work will be automatically thrown away.

Note that the Verilog semantics require that if a or b have any X/Z bits, then the answer should be X. This is true even when the X occurs in an insignificant place, e.g., 1000 > 000x is considered to be X even though no matter what the X digit is, we can see that the mathematical answer ought to be 1. (This behavior might be intended to give synthesis tools as much freedom as possible when implementing the operation.)

Definitions and Theorems

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

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

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

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

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

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