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
Vl-alias-fix
Vl-alias-p
Vl-alias-equiv
Make-vl-alias
Change-vl-alias
Vl-alias->rhs
Vl-alias->loc
Vl-alias->lhs
Vl-alias->atts
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
Vwsim
Fgl
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Syntax
Vl-alias
Representation of an alias declaration.
This is a product type introduced by
defprod
.
Fields
lhs —
vl-expr
The left-hand side.
rhs —
vl-expr
The right-hand side.
atts —
vl-atts
Any attributes associated with this alias.
loc —
vl-location
Where the assignment was found in the source code.
Subtopics
Vl-alias-fix
Fixing function for
vl-alias
structures.
Vl-alias-p
Recognizer for
vl-alias
structures.
Vl-alias-equiv
Basic equivalence relation for
vl-alias
structures.
Make-vl-alias
Basic constructor macro for
vl-alias
structures.
Change-vl-alias
Modifying constructor for
vl-alias
structures.
Vl-alias->rhs
Get the
rhs
field from a
vl-alias
.
Vl-alias->loc
Get the
loc
field from a
vl-alias
.
Vl-alias->lhs
Get the
lhs
field from a
vl-alias
.
Vl-alias->atts
Get the
atts
field from a
vl-alias
.