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
Sv
Vwsim
Fgl
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-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-context1-fix
Vl-context1-equiv
Vl-context1-p
Make-vl-context1
Vl-context1->elem
Change-vl-context1
Vl-context1->mod
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
Syntax
Vl-context1
Description of where an expression occurs.
This is a product type introduced by
defprod
.
Fields
mod —
stringp
The module where this module element was taken from.
elem —
vl-ctxelement
Some element from the module.
Subtopics
Vl-context1-fix
Fixing function for
vl-context1
structures.
Vl-context1-equiv
Basic equivalence relation for
vl-context1
structures.
Vl-context1-p
Recognizer for
vl-context1
structures.
Make-vl-context1
Basic constructor macro for
vl-context1
structures.
Vl-context1->elem
Get the
elem
field from a
vl-context1
.
Change-vl-context1
Modifying constructor for
vl-context1
structures.
Vl-context1->mod
Get the
mod
field from a
vl-context1
.