rtl2model
is a Python framework for modeling, synthesis, and verification of hardware designs.
It is an offshoot of a larger hardware lifting project: https://github.com/adwait/hwlifting/
The following pieces of software are used:
- SymbiYosys (tested with commit
5d19e46
with Yices 2 backend) - Verilator (tested on versions 4.212 and 4.110)
- cvc5 1.0.0 (
pip3 install cvc5
) prettytable
(pip3 install prettytable
)- [optional]
pytest
(pip3 install pytest
) - [optional]
pdoc
(pip3 install pdoc
) This project also uses custom forks of some packages to implement bugfixes and performance improvements. Rungit submodule init --update --recursive
to get the source code for those forks. - custom build of pyverilog (
pip3 install -e ./Pyverilog
) - custom build of pyvcd (
pip3 install -e ./pyvcd
)
Finally, run pip3 install -e .
in this directory to install the rtl2model
package. You can then run examples with python3 examples/rvmini.py
.
To build documentation, run pdoc rtl2model
.
designs
: submodule containing RTL, simulation, and model checking code for each design under testexamples
: example scripts for verifying designs, written using thertl2model
frameworkpyvcd
,Pyverilog
: git submodules for custom builds of dependenciesscripts
: various utility python and shell scriptssrc
: python source code forrtl2model
moduletests
: test cases forrtl2model