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
X86isa
Svl
Svex-simplify
Svexlist-simplify
Svex-alist-simplify
4vec-to-svex
4vec-to-svex-lst
Svl-flatten-design
Svl-run
Svl-run->svex-alist
Svex-to-verilog
Rtl
Software-verification
Math
Testing-utilities
4vec-to-svex
4vec-to-svex-lst
Signature
(4vec-to-svex-lst lst svexl-node-flg memoize-flg) → (mv err res-lst)