/rtl2model

a compositional framework for hardware lifting

Primary LanguagePython

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/

Installation

Dependencies

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)

Python packages

  • 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. Run git 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.

Structure

  • designs: submodule containing RTL, simulation, and model checking code for each design under test
  • examples: example scripts for verifying designs, written using the rtl2model framework
  • pyvcd, Pyverilog: git submodules for custom builds of dependencies
  • scripts: various utility python and shell scripts
  • src: python source code for rtl2model module
  • tests: test cases for rtl2model