Search-engine friendly clone of the
ACL2 documentation
.
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-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-enumitem-fix
Vl-enumitem-p
Vl-enumitem-equiv
Make-vl-enumitem
Vl-enumitem->value
Vl-enumitem->range
Vl-enumitem->name
Change-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
Vwsim
Fgl
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Syntax
Vl-enumitem
A single member of an
enum
.
This is a product type introduced by
defprod
.
Fields
name —
stringp
range —
vl-maybe-range
value —
vl-maybe-expr
Subtopics
Vl-enumitem-fix
Fixing function for
vl-enumitem
structures.
Vl-enumitem-p
Recognizer for
vl-enumitem
structures.
Vl-enumitem-equiv
Basic equivalence relation for
vl-enumitem
structures.
Make-vl-enumitem
Basic constructor macro for
vl-enumitem
structures.
Vl-enumitem->value
Get the
value
field from a
vl-enumitem
.
Vl-enumitem->range
Get the
range
field from a
vl-enumitem
.
Vl-enumitem->name
Get the
name
field from a
vl-enumitem
.
Change-vl-enumitem
Modifying constructor for
vl-enumitem
structures.