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.
0 comments:
Post a Comment