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
Rewriting
Svex
Svar
Least-fixpoint
Svex-p
Svex-select
Svex-alist
Svex-equiv
Svexlist
Svex-call
Fnsym
Svex-quote
Svex-var
Svcall-rw
Svcall
Svex-kind
Svcall*
Svex-fix
Svex-count
Svex-1z
Svex-1x
Svex-z
Svex-x
Bit-blasting
Functions
4vmask
Why-infinite-width
Svex-vars
Evaluation
Values
Symbolic-test-vector
Vl-to-svex
Vwsim
Fgl
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Svex
Svex-p
Recognizer for
svex
structures.
Signature
(svex-p x) → *