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
Loader
Warnings
Getting-started
Utilities
Printer
Kit
Mlib
Scopestack
Hid-tools
Vl-follow-hidexpr
Vl-index-expr-typetrace
Vl-follow-scopeexpr
Vl-follow-hidexpr-dimscheck
Vl-datatype-resolve-selects
Vl-datatype-remove-dim
Vl-operandinfo
Vl-follow-hidexpr-dimcheck
Vl-follow-data-selects
Vl-follow-hidexpr-error
Vl-hidstep
Vl-scopestack-find-item/ss/path
Vl-follow-array-indices
Vl-scopecontext
Vl-datatype-set-unsigned
Vl-selstep
Vl-scopestack-find-elabpath
Vl-hid-prefix-for-subhid
Vl-find-structmember
Vl-select
Vl-scopeexpr-replace-hid
Vl-genblocklist-find-block
Vl-partselect-width
Vl-seltrace->indices
Vl-datatype->structmembers
Vl-hidexpr-resolved-p
Vl-operandinfo->indices
Vl-flatten-hidindex
Vl-subhid-p
Vl-seltrace-usertypes-ok
Vl-flatten-hidexpr
Vl-scopeexpr->hid
Vl-seltrace-index-count
Vl-operandinfo-usertypes-ok
Vl-operandinfo-index-count
Vl-datatype-dims-count
Vl-scopeexpr-index-count
Vl-hidexpr-index-count
Vl-usertype-lookup
Vl-hidindex-resolved-p
Vl-scopeexpr-resolved-p
Vl-selstep-usertypes-ok
Vl-hidtrace
Vl-seltrace
Vl-seltrace-fix
Vl-seltrace-equiv
Vl-seltrace-p
Vl-scopedef-interface-p
Filtering-by-name
Vl-interface-mocktype
Stripping-functions
Genblob
Expr-tools
Extract-vl-types
Hierarchy
Range-tools
Finding-by-name
Stmt-tools
Modnamespace
Flat-warnings
Reordering-by-name
Datatype-tools
Syscalls
Allexprs
Lvalues
Port-tools
Transforms
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Hid-tools
Vl-seltrace
A list of
vl-selstep-p
objects.
This is an ordinary
fty::deflist
.
Subtopics
Vl-seltrace-fix
(vl-seltrace-fix x)
is a usual
fty
list fixing function.
Vl-seltrace-equiv
Basic equivalence relation for
vl-seltrace
structures.
Vl-seltrace-p
(vl-seltrace-p x)
recognizes lists where every element satisfies
vl-selstep-p
.