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-atts
Vl-expr
Vl-expr-p
Vl-expr->atts
Vl-index
Vl-scopeexpr
Vl-scopeexpr-p
Vl-scopeexpr-colon
Vl-scopeexpr-colon->paramargs
Vl-scopeexpr-colon->rest
Make-vl-scopeexpr-colon
Vl-scopeexpr-colon->first
Change-vl-scopeexpr-colon
Vl-scopename
Vl-scopename-equiv
Vl-scopename-fix
Vl-scopename-p
Vl-scopenamelist
Vl-scopenamelist-fix
Vl-scopenamelist-equiv
Vl-scopenamelist-p
Vl-scopeexpr-equiv
Vl-scopeexpr-end
Vl-scopeexpr->expr
Vl-scopeexpr-kind
Vl-scopeexprlist
Vl-scopeexpr-fix
Vl-scopeexpr-count
Vl-hidindex
Vl-partselect
Vl-hidexpr
Make-vl-index
Vl-index->indices
Vl-index->scope
Vl-index->part
Vl-index->atts
Change-vl-index
Vl-scopeexpr->expr
Vl-hidname
Vl-call
Vl-exprsign
Vl-maybe-expr
Vl-stream
Vl-expr-case
Vl-pattern
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-scopename
Vl-scopenamelist
A list of
vl-scopename-p
objects.
This is an ordinary
fty::deflist
.
Subtopics
Vl-scopenamelist-fix
(vl-scopenamelist-fix x)
is a usual
fty
list fixing function.
Vl-scopenamelist-equiv
Basic equivalence relation for
vl-scopenamelist
structures.
Vl-scopenamelist-p
(vl-scopenamelist-p x)
recognizes lists where every element satisfies
vl-scopename-p
.