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
Filtering-by-name
Vl-interface-mocktype
Stripping-functions
Genblob
Expr-tools
Vl-expr-typedecide
Vl-exprlist-resolved->vals
Vl-make-idexpr-list
Vl-idexprlist->names
Vl-expr-selfsize
Vl-expr-update-subexprs
Vl-exprlist-to-plainarglist
Vl-call-namedargs-update-subexprs
Vl-valuerangelist-update-subexprs
Vl-streamexprlist-update-subexprs
Vl-op-p
Vl-maybe-exprlist-update-subexprs
Vl-evatomlist-update-subexprs
Vl-expr-values
Vl-keyvallist-update-subexprs
Vl-assignpat-update-subexprs
Vl-valuerange-update-subexprs
Vl-scopeexpr-update-subexprs
Vl-partselect-update-subexprs
Vl-hidexpr-update-subexprs
Vl-expr-add-atts
Vl-arrayrange-update-subexprs
Vl-streamexpr-update-subexprs
Vl-slicesize-update-subexprs
Vl-plusminus-update-subexprs
Vl-patternkey-update-subexprs
Vl-expr-ops
Vl-make-integer
Vl-range-update-subexprs
Vl-idexpr
Vl-make-index
Vl-expr->subexprs
Vl-bitlist-from-nat
Vl-pps-expr
Vl-maybe-exprlist->subexprs
Vl-hidexpr->subexprs
Vl-evatomlist->subexprs
Vl-call-namedargs->subexprs
Vl-valuerangelist->subexprs
Vl-streamexprlist->subexprs
Vl-keyvallist->subexprs
Vl-exprlist-has-ops
Vl-expr-resolved-p
Vl-valuerange->subexprs
Vl-streamexpr->subexprs
Vl-slicesize->subexprs
Vl-scopeexpr->subexprs
Vl-patternkey->subexprs
Vl-partselect->subexprs
Vl-assignpat->subexprs
Vl-arrayrange->subexprs
Vl-pps-origexpr
Vl-plusminus->subexprs
Vl-idscope
Vl-idexpr->name
Vl-expr-has-ops
Vl-resolved->val
Vl-range->subexprs
Vl-idexpr-p
Vl-idexprlist-p
Vl-exprlist-resolved-p
Vl-idscope->name
Vl-idscope-p
Vl-zbitlist-p
Vl-zatom-p
Vl-op-fix
Vl-oplist
Vl-expr-varnames
Vl-one-bit-constants
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
Mlib
Expr-tools
Basic functions for working with expressions.
Subtopics
Vl-expr-typedecide
Determine the arithmetic class (signed or unsigned integer, shortreal or real, or something else) of an top-level or self-determined expression.
Vl-exprlist-resolved->vals
(vl-exprlist-resolved->vals x)
maps
vl-resolved->val
across a list.
Vl-make-idexpr-list
(vl-make-idexpr-list x)
maps
vl-idexpr
across a list.
Vl-idexprlist->names
(vl-idexprlist->names x)
maps
vl-idexpr->name
across a list.
Vl-expr-selfsize
Computation of self-determined expression sizes.
Vl-expr-update-subexprs
Vl-exprlist-to-plainarglist
Convert expressions into
vl-plainarg-p
s.
Vl-call-namedargs-update-subexprs
Vl-valuerangelist-update-subexprs
Vl-streamexprlist-update-subexprs
Vl-op-p
Vl-maybe-exprlist-update-subexprs
Vl-evatomlist-update-subexprs
Vl-expr-values
Gather all of the values throughout an expression.
Vl-keyvallist-update-subexprs
Vl-assignpat-update-subexprs
Vl-valuerange-update-subexprs
Vl-scopeexpr-update-subexprs
Vl-partselect-update-subexprs
Vl-hidexpr-update-subexprs
Vl-expr-add-atts
Vl-arrayrange-update-subexprs
Vl-streamexpr-update-subexprs
Vl-slicesize-update-subexprs
Vl-plusminus-update-subexprs
Vl-patternkey-update-subexprs
Vl-expr-ops
Gather all of the operators used throughout an expression.
Vl-make-integer
Safely create a well-typed constant integer atom whose value is n.
Vl-range-update-subexprs
Vl-idexpr
Construct an
vl-idexpr-p
.
Vl-make-index
Safely create a constant integer atom whose value is n.
Vl-expr->subexprs
Vl-bitlist-from-nat
Turn a natural number into a vl-bitlist-p of the given width.
Vl-pps-expr
Pretty-print an expression into a string.
Vl-maybe-exprlist->subexprs
Vl-hidexpr->subexprs
Vl-evatomlist->subexprs
Vl-call-namedargs->subexprs
Vl-valuerangelist->subexprs
Vl-streamexprlist->subexprs
Vl-keyvallist->subexprs
Vl-exprlist-has-ops
Vl-expr-resolved-p
Recognizes plain constant integer expressions.
Vl-valuerange->subexprs
Vl-streamexpr->subexprs
Vl-slicesize->subexprs
Vl-scopeexpr->subexprs
Vl-patternkey->subexprs
Vl-partselect->subexprs
Vl-assignpat->subexprs
Vl-arrayrange->subexprs
Vl-pps-origexpr
Pretty-print the "original," un-transformed version of an expression into a string.
Vl-plusminus->subexprs
Vl-idscope
Vl-idexpr->name
Get the name from a
vl-idexpr-p
.
Vl-expr-has-ops
Vl-resolved->val
Get the value from a resolved expression.
Vl-range->subexprs
Vl-idexpr-p
Recognize plain identifier expressions.
Vl-idexprlist-p
(vl-idexprlist-p x)
recognizes lists where every element satisfies
vl-idexpr-p
.
Vl-exprlist-resolved-p
(vl-exprlist-resolved-p x)
recognizes lists where every element satisfies
vl-expr-resolved-p
.
Vl-idscope->name
Vl-idscope-p
Recognize a scopeexpr that is just a plain identifier.
Vl-zbitlist-p
Vl-zatom-p
Vl-op-fix
Vl-oplist
A list of
vl-op-p
objects.
Vl-expr-varnames
Extract all the variable names from a VL expression.
Vl-one-bit-constants
Already-sized, one-bit constants.