This repository contains examples for verification of RTL designs with operational models.
Note that running the examples in this repository will require an installation of SymbiYosys. Please follow the installation instructions.
Currently backend solvers have been configured to be boolector for BMC proofs and abc for PDR proofs. The installation instructions for these can also be found at the above link. Alternatively, you can try different solvers too (refer to above link for details). All installed software should be on your $PATH.
Once all requirements (SymbiYosys and solvers) are satisfied, the examples can be run either by executing the main script run-main.sh or each example script individually. Enjoy!