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
Svex-stvs
Svex-decomposition-methodology
Sv-versus-esim
Svex-decomp
Svex-compose-dfs
Svex-compilation
Moddb
Svmods
Svstmt
Sv-tutorial
Expressions
Symbolic-test-vector
Vl-to-svex
Vl-to-sv
Vl-design->sv-design
Vl-simpconfig
Vl-hierarchy-sv-translation
Vl-expr-svex-translation
Vl-design->svex-modalist
Vl-svstmt
Vl-svstmt.lisp
Vl-casestmt-violation-conds
Vl-caselist-none/multiple
Vl-elaborated-expr-consteval
Vl-always->svex
Vl-caseexprs->svex-test
Vl-always->svex-checks
Vl-implicitvalueparam-final-type
Vl-assignstmt->svstmts
Vl-fundecl-to-svex
Vl-evatomlist-delay-substitution
Vl-consteval
Vl-alwayslist->svex
Vl-index-expr-svex/size/type
Vl-vardecllist->svstmts
Sv::svex-alist->assigns
Vl-case-conservative-test-expr
Vl-evatomlist->svex
Vl-case-xcond-wrapper
Sv::constraintlist-maybe-rewrite-fixpoint
Vl-always-apply-trigger-to-updates
Vl-initiallist-size-warnings
Vl-initial-size-warnings
Vl-finallist-size-warnings
Vl-always->svex-latch-warnings
Vl-final-size-warnings
Sv::svarlist-masked-x-subst
Sv::svar->lhs-by-mask
Svstmt-config
Sv::svex-alist-unset-nonblocking
Sv::svar->lhs-by-size
Combine-mask-alists
Sv::svarlist-delay-subst
Vttree-constraints-to-svstmts
Sv::4vmask-alist-unset-nonblocking
Sv::svarlist-remove-delays
Vl-caselist->caseexprs
Vl-evatomlist-has-edge
Vl-to-sv-main
Vl-simplify-sv
Vl-user-paramsettings->unparam-names
Vl-user-paramsettings->modnames
Vwsim
Fgl
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Vl-svstmt
Vl-svstmt.lisp
Subtopics
Vl-casestmt-violation-conds
Vl-caselist-none/multiple
Vl-elaborated-expr-consteval
Assumes expression is already elaborated.
Vl-always->svex
Translate a combinational or latch-type always block into a set of SVEX expressions.
Vl-caseexprs->svex-test
Vl-always->svex-checks
Checks that the always block is suitable for translating to svex, ~ and returns the body statement and eventcontrol.
Vl-implicitvalueparam-final-type
Vl-assignstmt->svstmts
Vl-fundecl-to-svex
Vl-evatomlist-delay-substitution
Vl-consteval
Vl-alwayslist->svex
Translate a combinational or latch-type always block into a set of SVEX expressions.
Vl-index-expr-svex/size/type
Vl-vardecllist->svstmts
Sv::svex-alist->assigns
Given an svex alist, return an assignment alist, i.e. transform the bound variables into LHSes based on the given masks, which represent the bits of the variables that are supposed to be written.
Vl-case-conservative-test-expr
Vl-evatomlist->svex
Vl-case-xcond-wrapper
Sv::constraintlist-maybe-rewrite-fixpoint
Vl-always-apply-trigger-to-updates
Vl-initiallist-size-warnings
Vl-initial-size-warnings
Generate any sizing warnings for an initial statement.
Vl-finallist-size-warnings
Vl-always->svex-latch-warnings
Vl-final-size-warnings
Generate any sizing warnings for an final statement.
Sv::svarlist-masked-x-subst
Sv::svar->lhs-by-mask
Given a variable and a mask of bits, create an LHS that covers those bits.
Svstmt-config
Sv::svex-alist-unset-nonblocking
Sv::svar->lhs-by-size
Given a variable and a size in bits, create an LHS that covers those bits.
Combine-mask-alists
Sv::svarlist-delay-subst
Creates a substitution alist that maps the given variables to their 1-tick delayed versions. Warns if the variables aren't of the expected form.
Vttree-constraints-to-svstmts
Sv::4vmask-alist-unset-nonblocking
Sv::svarlist-remove-delays
Vl-caselist->caseexprs
Vl-evatomlist-has-edge