Hardware-verification
Libraries for working with hardware description languages, modeling
circuits, etc.
Also see the (probably incomplete)
page
of ACL2-related publications.
Subtopics
- Gl
- A symbolic simulation framework for proving finitely bounded ACL2
theorems by bit-blasting with a Binary Decision
Diagram (BDD) package or a SAT
solver.
- Esim
- 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.
- Vl2014
- The VL Verilog Toolkit, 2014 Edition. This is a "stable" fork of
vl for compatibility with esim.
- Sv
- 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.
- Fgl
- A prover framework that supports bit-blasting.
- Vwsim
- A circuit simulator for rapid, single-flux, quantum
circuits.
- Vl
- 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.
- X86isa
- x86 ISA model and machine-code analysis framework developed
at UT Austin.
- Svl
- A framework to simulate Verilog designs with retained design hiearchy
- Rtl
- A library of register-transfer logic and computer arithmetic
