cores
/
power-fv
3
1
Fork 0
Code Issues 18 Pull Requests Projects Releases Wiki Activity
You cannot select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
103 Commits
2 Branches
0 Tags
251 KiB
Python 100%
 
dinofly
main
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from 'd687a9a511'
${ noResults }
Go to file
Jean-François Nguyen d687a9a511 insn: fix TAR SPR number. 2 years ago
cores/microwatt pfv: add configurable memory alignment constraints. 2 years ago
power_fv insn: fix TAR SPR number. 2 years ago
.gitignore initial push with a gitignore file 3 years ago
LICENSE.txt Add license. 3 years ago
README.md README: fix styling, update microwatt URL. 2 years ago
poetry.lock Add support for remote builds over SSH. 2 years ago
pyproject.toml Update README. 2 years ago

README.md
Unescape Escape

POWER-FV – Assertion-based formal verification library for OpenPOWER processors

Disclaimer

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

Overview

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.

Testbenches and behavioral models are implemented in Python using Amaranth HDL, and SymbiYosys for its formal verification flow. Processor cores may use any HDL supported by Yosys.

POWER-FV's design is heavily inspired by the riscv-formal framework, developed by Claire Wolf (YosysHQ).

Prerequisites

If VHDL support is needed:

The OSS CAD Suite can provide pre-built binaries of these tools.

Installation

pip3 install poetry --user
poetry install

Examples

See the cores folder for usage examples.