ACL2 Guide to Logic and Programming Language:Hardware-verification

Libraries for working with hardware description languages, modeling circuits, etc.

Also see the (probably incomplete) page of ACL2-related publications.

Subtopics

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.

Fgl

A prover framework that supports bit-blasting.

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.

Rtl

A library of register-transfer logic and computer arithmetic

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.

Svl

A framework to simulate Verilog designs with retained design hiearchy

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.

Vl2014

The VL Verilog Toolkit, 2014 Edition. This is a "stable" fork of vl for compatibility with esim.

Vwsim

A circuit simulator for rapid, single-flux, quantum circuits.

X86isa

x86 ISA model and machine-code analysis framework developed at UT Austin.