Libraries for working with hardware description languages, modeling
Also see the (probably incomplete) page
of ACL2-related publications
- A symbolic simulation framework for proving finitely bounded ACL2
theorems by bit-blasting with a Binary Decision
Diagram (BDD) package or a SAT
- ESIM is a simple, hierarchical, bit-level, cycle-based,
register-transfer level hardware description language. It is based on a clean,
monotonic four-valued logic (see 4v) and features strong support
for symbolic simulation with gl.
- The VL Verilog Toolkit, 2014 Edition. This is a "stable" fork of
vl for compatibility with esim.
- SV is a hardware verification library that features a vector-based
expression representation (svex), efficient symbolic simulation that is
integrated with gl, and support for many SystemVerilog features. It
generally replaces esim as a backend for vl.
- A prover framework that supports bit-blasting.
- The VL Verilog Toolkit is a large ACL2 library for working with SystemVerilog (and also
regular Verilog) source
code, developed at Centaur Technology by
Jared Davis and Sol Swords. It serves as a frontend for many Verilog tools.
- A framework to simulate Verilog designs with retained design hiearchy
- A library of register-transfer logic and computer arithmetic