		Search-engine friendly clone of the ACL2 documentation.

Occform

vl-1-bit-signed-gte

Degenerate, single-bit signed greater-than-or-equal module.

This is a gate-based module that is semantically equivalent to:

module VL_1_BIT_SIGNED_GTE (out, a, b);
  output out;
  input signed a;
  input signed b;

  assign out = a >= b;
endmodule

Since Verilog uses 2's complement as its representation of signed numbers, in the degenerate world of sign-bits we should have "0 means 0 and 1 means -1". So, counterintuitively, a >= b holds except when a = 1 and b = 0.

Warning: The above is indeed the behavior implemented by NCVerilog. But Verilog-XL appears to be buggy and instead produces results that are consistent with an unsigned interpretation; see tests/test-scomp.v.

Our actual module is:

module VL_1_BIT_SIGNED_GTE (out, a, b);
  output out;
  input a, b;
  wire bbar, mainbar, main, xa, xb, xab;

  not(bbar, b);                    // assign main = ~(a & ~b)
  and(mainbar, a, bbar);
  not(main, mainbar);

  xor(xb, b, b);                   // Propagate Xes
  xor(xa, a, a);
  xor(xab, xa, xb);
  xor(out, xab, main);
endmodule

Definition: *vl-1-bit-signed-gte*

(defconst *vl-1-bit-signed-gte*
 (b*
  ((name (hons-copy "VL_1_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-primitive-mkport "a" :vl-input))
   ((mv b-expr b-port b-portdecl b-vardecl)
    (vl-primitive-mkport "b" :vl-input))
   ((mv bbar-expr bbar-vardecl)
    (vl-primitive-mkwire "bbar"))
   ((mv mainbar-expr mainbar-vardecl)
    (vl-primitive-mkwire "mainbar"))
   ((mv main-expr main-vardecl)
    (vl-primitive-mkwire "main"))
   ((mv xa-expr xa-vardecl)
    (vl-primitive-mkwire "xa"))
   ((mv xb-expr xb-vardecl)
    (vl-primitive-mkwire "xb"))
   ((mv xab-expr xab-vardecl)
    (vl-primitive-mkwire "xab"))
   (bbar-inst (vl-simple-inst *vl-1-bit-not*
                              "mk_bbar" bbar-expr b-expr))
   (mainbar-inst (vl-simple-inst *vl-1-bit-and* "mk_mainbar"
                                 mainbar-expr a-expr bbar-expr))
   (main-inst (vl-simple-inst *vl-1-bit-not*
                              "mk_main" main-expr mainbar-expr))
   (xb-inst (vl-simple-inst *vl-1-bit-xor*
                            "mk_xb" xb-expr b-expr b-expr))
   (xa-inst (vl-simple-inst *vl-1-bit-xor*
                            "mk_xa" xa-expr a-expr a-expr))
   (xab-inst (vl-simple-inst *vl-1-bit-xor*
                             "mk_xab" xab-expr xa-expr xb-expr))
   (out-inst (vl-simple-inst *vl-1-bit-xor*
                             "mk_out" out-expr xab-expr main-expr)))
  (hons-copy
       (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 bbar-vardecl
                            mainbar-vardecl main-vardecl
                            xa-vardecl xb-vardecl xab-vardecl)
            :modinsts (list bbar-inst mainbar-inst main-inst
                            xa-inst xb-inst xab-inst out-inst)
            :minloc *vl-fakeloc*
            :maxloc *vl-fakeloc*))))