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
Svstmt-config-fix
Svstmt-config-equiv
Make-svstmt-config
Svstmt-config->uniquecase-constraints
Svstmt-config->uniquecase-conservative
Svstmt-config->nonblockingp
Change-svstmt-config
Svstmt-config-p
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.lisp
Svstmt-config
This is a product type introduced by
defprod
.
Fields
nonblockingp —
booleanp
uniquecase-conservative —
natp
uniquecase-constraints —
booleanp
Subtopics
Svstmt-config-fix
Fixing function for
svstmt-config
structures.
Svstmt-config-equiv
Basic equivalence relation for
svstmt-config
structures.
Make-svstmt-config
Basic constructor macro for
svstmt-config
structures.
Svstmt-config->uniquecase-constraints
Get the
uniquecase-constraints
field from a
svstmt-config
.
Svstmt-config->uniquecase-conservative
Get the
uniquecase-conservative
field from a
svstmt-config
.
Svstmt-config->nonblockingp
Get the
nonblockingp
field from a
svstmt-config
.
Change-svstmt-config
Modifying constructor for
svstmt-config
structures.
Svstmt-config-p
Recognizer for
svstmt-config
structures.