• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
        • Primitives
        • Use-set
        • Syntax
          • Vl-module
          • Vl-vardecl
          • Expressions
            • Vl-atts
            • Vl-constint
              • Vl-constint-fix
              • Vl-constint-p
              • Vl-constint-equiv
              • Make-vl-constint
              • Vl-constint->origtype
              • Vl-constint->value
              • Vl-constint->wasunsized
              • Vl-constint->origwidth
              • Change-vl-constint
            • *vl-ops-table*
            • Vl-weirdint
            • Vl-expr
            • Vl-id
            • Vl-hidpiece
            • Vl-time
            • Vl-maybe-exprtype
            • Vl-op-p
            • Vl-maybe-expr
            • Vl-expr->finaltype
            • Vl-real
            • Vl-expr->finalwidth
            • Vl-tagname
            • Vl-sysfunname
            • Vl-string
            • Vl-op-arity
            • Vl-keyguts
            • Vl-exprtype-p
            • Vl-typename
            • Vl-funname
            • Vl-basictype
            • Vl-extint
            • Vl-atomlist-p
            • Vl-atomguts
            • Vl-nbits-fix
            • Vl-atom-p
            • Vl-arity-fix
            • Vl-arity-ok-p
            • Vl-op-text
            • Vl-exprlist
            • Vl-oplist
            • Vl-exprlistlist
            • Vl-ops-table
            • *vl-default-expr*
          • Vl-fundecl
          • Vl-assign
          • Vl-gateinst
          • Vl-modinst
          • Vl-commentmap
          • Vl-portdecl
          • Vl-taskdecl
          • Vl-design
          • Vl-interface
          • Vl-plainarglist->exprs
          • Vl-taskdecllist->names
          • Vl-fundecllist->names
          • Vl-package
          • Vl-port
          • Vl-udp
          • Vl-paramdecl
          • Vl-genelement
          • Vl-cycledelayrange
          • Vl-namedarg
          • Vl-sort-blockitems-aux
          • Vl-distitem
          • Vl-gatedelay
          • Vl-repetition
          • Vl-typedef
          • Vl-range
          • Vl-gatestrength
          • Vl-program
          • Vl-config
          • Vl-always
          • Vl-datatype-update-dims
          • Vl-import
          • Vl-enumbasetype
          • Vl-repeateventcontrol
          • Vl-paramargs
          • Vl-initial
          • Vl-eventcontrol
          • Vl-udpsymbol-p
          • Vl-maybe-range
          • Vl-maybe-nettypename
          • Vl-maybe-gatestrength
          • Vl-maybe-gatedelay
          • Vl-maybe-delayoreventcontrol
          • Vl-alias
          • Maybe-string-fix
          • Vl-maybe-packeddimension
          • Vl-fwdtypedef
          • Vl-evatom
          • Vl-packeddimension-p
          • Vl-maybe-udpsymbol
          • Vl-maybe-module
          • Vl-maybe-direction
          • Vl-maybe-datatype
          • Vl-maybe-cstrength
          • Vl-direction-p
          • Vl-arguments
          • Vl-maybe-design
          • Vl-udpline
          • Vl-exprdist
          • Vl-context1
          • Vl-genvar
          • Vl-enumitem
          • Vl-datatype-update-udims
          • Vl-datatype-update-pdims
          • Vl-modelement
          • Vl-udpedge
          • Vl-delaycontrol
          • Vl-context
          • Vl-sort-blockitems
          • Vl-distweighttype-p
          • Vl-ctxelement->loc
          • Vl-blockitem
          • Vl-vardecllist
          • Vl-module->ifports
          • Vl-modelement->loc
          • Vl-ctxelement
          • Vl-coretypename-p
          • Vl-packeddimensionlist
          • Vl-modelementlist->genelements
          • Vl-gatetype-p
          • Vl-paramdecllist
          • Vl-lifetime-p
          • Vl-datatype->udims
          • Vl-datatype->pdims
          • Vl-timeunit-p
          • Vl-repetitiontype-p
          • Vl-port->name
          • Vl-importlist
          • Vl-genelement->loc
          • Vl-delayoreventcontrol
          • Vl-cstrength-p
          • Statements
          • Vl-udpentry-p
          • Vl-packeddimension-fix
          • Vl-nettypename-p
          • Vl-portdecllist
          • Vl-port->loc
          • Vl-enumbasekind-fix
          • Vl-arguments->args
          • Vl-taskdecllist
          • Vl-portlist
          • Vl-importpart-p
          • Vl-importpart-fix
          • Vl-fundecllist
          • Vl-blockstmt-p
          • Vl-assignlist
          • Vl-alwaystype-p
          • Vl-typedeflist
          • Vl-syntaxversion-p
          • Vl-randomqualifier-p
          • Vl-modinstlist
          • Vl-gateinstlist
          • Vl-blockitemlist
          • Vl-udptable
          • Vl-udplist
          • Vl-udpentrylist
          • Vl-programlist
          • Vl-paramvaluelist
          • Vl-packagelist
          • Vl-namedparamvaluelist
          • Vl-namedarglist
          • Vl-modulelist
          • Vl-modportlist
          • Vl-modport-portlist
          • Vl-interfacelist
          • Vl-initiallist
          • Vl-genvarlist
          • Vl-fwdtypedeflist
          • Vl-evatomlist
          • Vl-enumitemlist
          • Vl-distlist
          • Vl-configlist
          • Vl-alwayslist
          • Vl-aliaslist
          • Vl-regularportlist
          • Vl-rangelist-list
          • Vl-rangelist
          • Vl-paramdecllist-list
          • Vl-modelementlist
          • Vl-maybe-range-list
          • Vl-interfaceportlist
          • Vl-argumentlist
          • Data-types
        • Getting-started
        • Utilities
        • Loader
        • Transforms
        • Lint
        • Mlib
        • Server
        • Kit
        • Printer
        • Esim-vl
        • Well-formedness
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Expressions

Vl-constint

Representation for constant integer literals with no X or Z bits.

This is a product type introduced by defprod.

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.
origtype — vl-exprtype-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:

(< value (expt 2 origwidth))

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 origtype fields are subtle. They indicate the original width and signedness of the literal as specified in the source code, e.g., if the source code contains 8'sd 65, then the origwidth will be 8 and the origtype will be :vl-signed. These fields are subtle because expression-sizing generally alters the widths and types of subexpressions, so these may not represent the final widths and types of these constants in the context of the larger expression. Instead, the preferred way to determine a constint's final width and sign is to inspect the vl-atom-p that contains it.

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 from the left, as required by Section 3.5.1 (page 10) of the Verilog-2005 standard.

Note that in Verilog, unsized integer constants like 5 or 'b101 have an implementation-dependent size of at least 32 bits. VL historically 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. On the other hand, some 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 later 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

Vl-constint-fix
Fixing function for vl-constint structures.
Vl-constint-p
Recognizer for vl-constint structures.
Vl-constint-equiv
Basic equivalence relation for vl-constint structures.
Make-vl-constint
Basic constructor macro for vl-constint structures.
Vl-constint->origtype
Get the origtype field from a vl-constint.
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.
Change-vl-constint
Modifying constructor for vl-constint structures.