• 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
                  • Vl-weirdint
                    • Vl-bitlist-nonempty-fix
                    • Vl-weirdint->bits
                    • Make-vl-weirdint
                    • Vl-weirdint->wasunsized
                    • Vl-weirdint->origsign
                    • Vl-bit
                    • Change-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-weirdint

Representation for constant integer literals with any X or Z bits, e.g., 4'b11xx.

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

Fields
bits — vl-bitlist
An MSB-first list of the four-valued Verilog bits making up this constant's value; see vl-bit-p.
origsign — vl-exprsign-p
Subtle; generally should not be used; see below.
wasunsized — booleanp
Did this constant have an explicit size?
Additional Requirements

The following invariant is enforced on the fields:

(consp bits)

Detailed Explanation

Weird integers are produced by source code constructs like 1'bz, 3'b0X1, and so on.

Weirdints are mostly like vl-constints except that instead of having a natural number value they have bits, a list of four-valued vl-bits, which are always represented in MSB-first order.

The origsign and wasunsized fields are analogous to those from a vl-constint; see the discussion there for details.

Unlike a constint, a weirdint has no origwidth. Instead, its original width is implicitly just the length of its bits. When our lexer encounters a weirdint like 5'b1x, it automatically extends it to the desired width; see for instance vl-correct-bitlist. Note that, as with constints, you usually should not be looking at this length or at the origsign field, because these original values are not necessarily the correct post-sizing sizes and signedness.

Like constinsts, all weirdints are automatically constructed with hons. This may not be worthwhile since there are probably usually not too many weirdints, but by the same reasoning it shouldn't be too harmful.

Subtopics

Vl-bitlist-nonempty-fix
Fixing function for non-empty vl-bitlists.
Vl-weirdint->bits
Get the bits field from a vl-weirdint.
Make-vl-weirdint
Basic constructor macro for vl-weirdint structures.
Vl-weirdint->wasunsized
Get the wasunsized field from a vl-weirdint.
Vl-weirdint->origsign
Get the origsign field from a vl-weirdint.
Vl-bit
Representation of a single Verilog bit (0, 1, X, or Z).
Change-vl-weirdint
Modifying constructor for vl-weirdint structures.