• 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-ops-table*
            • Vl-weirdint
              • Vl-weirdint-fix
              • Vl-weirdint-p
              • Vl-weirdint-equiv
              • Make-vl-weirdint
              • Vl-weirdint->origtype
              • Vl-weirdint->bits
              • Vl-weirdint->wasunsized
              • Vl-weirdint->origwidth
              • Change-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-weirdint

Representation for constant integer literals with X or Z bits.

This is a product type introduced by defprod.

Fields
origwidth — posp
Subtle; generally should not be used; see below.
bits — vl-bitlist
An MSB-first list of the four-valued Verilog bits making up this constant's value; see vl-bit-p.
origtype — vl-exprtype-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:

(equal (len bits) origwidth)

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

The origwidth, origtype, and wasunsized fields are analogous to those from vl-constint-p; see the discussion there for details. But unlike a constint, a weirdint does not have a natural-number value. Instead it has a list of four-valued bits that may include X and Z values.

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