• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
        • Syntax
          • Vl-module
          • Vl-vardecl
          • Vl-fundecl
          • Vl-interface
          • Vl-design
          • Vl-assign
          • Vl-modinst
          • Vl-gateinst
          • Vl-taskdecl
          • Vl-portdecl
          • Vl-commentmap
          • Vl-dpiimport
          • Vl-ansi-portdecl
          • Vl-package
          • Vl-paramdecl
          • Vl-dpiexport
          • Vl-class
          • Vl-sort-blockitems-aux
          • Vl-plainarglist->exprs
          • Vl-taskdecllist->names
          • Expressions-and-datatypes
            • Vl-atts
            • Vl-expr
              • Vl-expr-p
              • Vl-expr->atts
              • Vl-index
              • Vl-call
              • Vl-exprsign
              • Vl-maybe-expr
              • Vl-stream
              • Vl-expr-case
              • Vl-pattern
              • Vl-literal
                • Vl-value
                  • Vl-constint
                    • Make-vl-constint
                    • Vl-constint->value
                    • Vl-constint->wasunsized
                    • Vl-constint->origwidth
                    • Vl-constint->origsign
                    • Change-vl-constint
                  • Vl-weirdint
                  • Vl-value-fix
                  • Vl-value-p
                  • Vl-value-case
                  • Vl-time
                  • Vl-real
                  • Vl-extint
                  • Vl-value-equiv
                  • Vl-string
                  • Vl-value-kind
                  • Vl-valuelist
                • Vl-literal->val
                • Vl-literal->atts
                • Make-vl-literal
                • Change-vl-literal
              • Vl-binary
              • Vl-expr-update-atts
              • Vl-unary
              • Vl-special
              • Vl-qmark
              • Vl-inside
              • Vl-cast
              • Vl-multiconcat
              • Vl-mintypmax
              • Vl-partselect-expr
              • Vl-bitselect-expr
              • Vl-tagged
              • Vl-concat
              • Vl-expr-equiv
              • Vl-eventexpr
              • Vl-expr-kind
              • Vl-exprlist
              • Vl-maybe-exprlist
              • Vl-expr-fix
              • Vl-expr-count
            • Vl-datatype
            • New-expression-representation
            • Vl-paramargs
            • Vl-evatom
            • Vl-maybe-paramargs
            • Vl-evatomlist
            • Vl-call-namedargs
            • Vl-paramvaluelist
            • Vl-namedparamvaluelist
          • Vl-fundecllist->names
          • Vl-udp
          • Vl-port
          • Vl-genelement
          • Vl-clkdecl
          • Vl-parse-temps
          • Vl-bind
          • Vl-namedarg
          • Vl-exprdist
          • Vl-clkassign
          • Vl-range
          • Vl-propport
          • Vl-typedef
          • Vl-gatedelay
          • Vl-dimension
          • Vl-sequence
          • Vl-clkskew
          • Vl-program
          • Vl-gatestrength
          • Vl-property
          • Vl-config
          • Vl-always
          • Vl-import
          • Vl-repeateventcontrol
          • Vl-timeliteral
          • Vl-initial
          • Vl-eventcontrol
          • Vl-final
          • Vl-udpsymbol-p
          • Vl-maybe-clkskew
          • Vl-function-specialization
          • Vl-alias
          • Vl-maybe-nettypename
          • Vl-maybe-gatedelay
          • Vl-letdecl
          • Vl-direction-p
          • Vl-modelement
          • Vl-maybe-timeprecisiondecl
          • Vl-maybe-scopeid
          • Vl-maybe-gatestrength
          • Vl-maybe-direction
          • Vl-maybe-delayoreventcontrol
          • Vl-gclkdecl
          • Vl-fwdtypedef
          • Vl-maybe-udpsymbol-p
          • Vl-maybe-timeunitdecl
          • Vl-maybe-timeliteral
          • Vl-maybe-parse-temps
          • Vl-maybe-cstrength
          • Vl-arguments
          • Vl-maybe-module
          • Vl-maybe-design
          • Vl-covergroup
          • Vl-udpline
          • Vl-timeunitdecl
          • Vl-genvar
          • Vl-defaultdisable
          • Vl-context1
          • Vl-timeprecisiondecl
          • Vl-sort-blockitems
          • Vl-elabtask
          • Vl-udpedge
          • Vl-delaycontrol
          • Vl-context
          • Vl-ctxelement
          • Vl-ctxelement->loc
          • Vl-modelement->loc
          • Statements
          • Vl-blockitem
          • Vl-vardecllist
          • Vl-interface->ifports
          • Vl-syntaxversion
          • Vl-nettypename-p
          • Vl-module->ifports
          • Vl-lifetime-p
          • Vl-paramdecllist
          • Vl-modelementlist->genelements
          • Vl-importlist
          • Vl-typedeflist
          • Vl-gatetype-p
          • Vl-cstrength-p
          • Vl-port->name
          • Vl-genelement->loc
          • Vl-delayoreventcontrol
          • Vl-udpentry-p
          • Vl-portdecllist
          • Vl-elabtask->loc
          • Property-expressions
          • Vl-taskdecllist
          • Vl-port->loc
          • Vl-fundecllist
          • Vl-sequencelist
          • Vl-propertylist
          • Vl-portlist
          • Vl-dpiimportlist
          • Vl-dpiexportlist
          • Vl-classlist
          • Vl-arguments->args
          • Vl-alwaystype-p
          • Vl-modinstlist
          • Vl-importpart-p
          • Vl-importpart-fix
          • Vl-bindlist
          • Vl-initiallist
          • Vl-genvarlist
          • Vl-gclkdecllist
          • Vl-function-specialization-map
          • Vl-finallist
          • Vl-elabtasklist
          • Vl-defaultdisablelist
          • Vl-clkdecllist
          • Vl-cassertionlist
          • Vl-blockstmt-p
          • Vl-assignlist
          • Vl-assertionlist
          • Vl-alwayslist
          • Vl-aliaslist
          • Vl-udptable
          • Vl-udplist
          • Vl-udpentrylist
          • Vl-propportlist
          • Vl-programlist
          • Vl-packagelist
          • Vl-namedarglist
          • Vl-modulelist
          • Vl-modportlist
          • Vl-modport-portlist
          • Vl-letdecllist
          • Vl-interfacelist
          • Vl-gateinstlist
          • Vl-fwdtypedeflist
          • Vl-covergrouplist
          • Vl-configlist
          • Vl-clkassignlist
          • Vl-blockitemlist
          • Vl-ansi-portdecllist
          • Vl-regularportlist
          • Vl-paramdecllist-list
          • Vl-modelementlist
          • Vl-interfaceportlist
          • Vl-casekey-p
          • Sv::maybe-4veclist
        • Loader
        • Warnings
        • Getting-started
        • Utilities
        • Printer
        • Kit
        • Mlib
        • Transforms
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Vl-value

Vl-constint

Representation for constant integer literals with no X or Z bits, e.g., 42, 5'b1, etc.

This is a product type, introduced by deftagsum in support of vl-value.

Fields
origwidth — posp
Subtle; generally should not be used; see below.
value — natp
The most important part of a constant integer. Even immediately upon parsing the value has already been determined and is available to you as an ordinary natural number.
origsign — vl-exprsign-p
Subtle; generally should not be used; see below.
wasunsized — booleanp
Set to t by the parser for unsized constants like 5 and 'b0101, but not for sized ones like 4'b0101.
Additional Requirements

The following invariant is enforced on the fields:

(unsigned-byte-p origwidth value)

Detailed Explanation

Constant integers are produced from source code constructs like 5, 4'b0010, and 3'h0.

Note that the value of a constant integer is never negative. In Verilog there are no negative literals; instead, an expression like -5 is basically parsed the same as -(5), so the negative sign is not part of the literal. See Section 3.5.1 of the Verilog-2005 standard.

The origwidth and origsign fields are subtle and you usually should not be looking at the origwidth and origsign of an expression unless you have really studied how sizing works in and you really know what you are doing.

These fields indicate the original width and signedness of the literal as specified in the source code. For instance, if the source code contains 8'sd 65, then we will get a value whose origwidth is 8 and whose origsign is :vl-signed. However, in general, the process for sizing Verilog expressions can effectively ``change'' the widths and types of the operands within that expression. For instance, if a and b are unsigned 10-bit wires and we have:

assign a = b + 3'sb1;

Then even though 3'sb1 looks like a signed 3-bit integer, the sizing process will convert it into a 10-bit unsigned number! The takeaway: you can't really rely on the original size and signedness to tell you the real story, so unless you're implementing the sizing algorithm you should probably avoid them.

We insist that 0 <= value <= 2^origwidth for every constant integer. If our lexer encounters something ill-formed like 3'b 1111, it emits a warning and truncates the value to the specified width as required by Section 3.5.1 (page 10) of the Verilog-2005 standard and Section 5.7.1 (page 37) of the SystemVerilog standard.

Note that in Verilog, unsized integer constants like 5 or 'b101 have an implementation-dependent size of at least 32 bits. Early versions of VL tried to treat such numbers in an abstract way, saying they had "integer size". But we eventually decided that this was too error-prone and we now instead act like a 32-bit implementation even at the level of our lexer. This conveniently makes the width of a constant integer just a positive number.

There is some risk to this. Certain expressions may produce different results on 32-bit versus, say, 64-bit implementations. Because of this, we added the wasunsized field so that we might, some day, statically check for problematic uses of unsized constants.

All constints are automatically created with hons. This is probably pretty trivial, but it seems nice. For instance, the constant integers from 0-32 are probably used thousands of times throughout a design for bit-selects and wire ranges, so sharing their memory may be useful.

Subtopics

Make-vl-constint
Basic constructor macro for vl-constint structures.
Vl-constint->value
Get the value field from a vl-constint.
Vl-constint->wasunsized
Get the wasunsized field from a vl-constint.
Vl-constint->origwidth
Get the origwidth field from a vl-constint.
Vl-constint->origsign
Get the origsign field from a vl-constint.
Change-vl-constint
Modifying constructor for vl-constint structures.