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.

41 lines
1.6 KiB

This file contains ambiguous Unicode characters!

This file contains ambiguous Unicode characters that may be confused with others in your current locale. If your use case is intentional and legitimate, you can safely ignore this warning. Use the Escape button to highlight these characters.

# 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
- Python 3.8+
- [Yosys](
- [SymbiYosys (sby)](
If VHDL support is needed:
- [GHDL](
- [ghdl-yosys-plugin](
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.