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-call
Vl-exprsign
Vl-maybe-expr
Vl-stream
Vl-arrayrange
Vl-streamexpr
Vl-slicesize
Vl-slicesize-case
Vl-slicesize-equiv
Vl-slicesize-type
Vl-slicesize-expr
Vl-slicesize-p
Vl-slicesize-none
Vl-slicesize-kind
Vl-slicesize-fix
Vl-slicesize-count
Make-vl-stream
Vl-stream->parts
Vl-stream->size
Vl-stream->dir
Vl-stream->atts
Change-vl-stream
Vl-leftright-p
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-slicesize
Vl-slicesize-count
Measure for recurring over
vl-slicesize
structures.
Signature
(vl-slicesize-count x) → count
Arguments
x
—
Guard
(
vl-slicesize-p
x)
.
Returns
count
—
Type
(
natp
count)
.