|Jean-François Nguyen e30ea40a8b||11 months ago|
|cores/microwatt||11 months ago|
|power_fv||11 months ago|
|.gitignore||1 year ago|
|LICENSE.txt||1 year ago|
|README.md||1 year ago|
|poetry.lock||1 year ago|
|pyproject.toml||1 year ago|
POWER-FV – Assertion-based formal verification library for OpenPOWER processors
This project is currently in an experimental state. In particular:
- it has only been tried on the Microwatt CPU
- it assumes an in-order scalar core
- its instruction coverage is limited to the Scalar Fixed-point Compliancy Subset
- the correctness of its own specifications hasn't yet been verified
POWER-FV is a formal verification library that can be used to check the compliance of a processor with the OpenPOWER ISA. It provides an interface to trace the execution of a processor, which is monitored by a testbench and compared against a given specification.
POWER-FV's design is heavily inspired by the riscv-formal framework, developed by Claire Wolf (YosysHQ).
If VHDL support is needed:
The OSS CAD Suite can provide pre-built binaries of these tools.
pip3 install poetry --user poetry install
cores folder for usage examples.