Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Recursion-and-induction
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
Hierarchy
Extract-vl-types
Range-tools
Finding-by-name
Stmt-tools
Modnamespace
Flat-warnings
Reordering-by-name
Datatype-tools
Vl-dimensionlist-total-size
Vl-maybe-usertype-resolve
Vl-dimensionlist-resolved-p
Vl-datatype-packedp
Vl-datatype-select-ok
Vl-dimension-size
Vl-datatype-size
Vl-maybe-dimension-size
Vl-hidexpr-name1
Maybe-nat-list
Syscalls
Allexprs
Lvalues
Port-tools
Transforms
X86isa
Svl
Rtl
Software-verification
Testing-utilities
Math
Mlib
Datatype-tools
Functions for working with datatypes.
Subtopics
Vl-dimensionlist-total-size
Given a dimensionlist like [5:0][3:1][0:8], multiplies the dimensions together to get the total number of bits, or returns nil if there are unsized dimensions (e.g., associative dimensions, queue dimensions, or dynamic array dimensions).
Vl-maybe-usertype-resolve
Vl-dimensionlist-resolved-p
Returns true if all sized dimensions are resolved.
Vl-datatype-packedp
Decide whether the datatype is packed or not.
Vl-datatype-select-ok
Determines whether this datatype can be selected.
Vl-dimension-size
Vl-datatype-size
Computes the number of bits in the datatype.
Vl-maybe-dimension-size
Vl-hidexpr-name1
Maybe-nat-list
A list of
maybe-natp
objects.
