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](https://github.com/amaranth-lang/amaranth), and [SymbiYosys](https://github.com/YosysHQ/sby) 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](https://github.com/YosysHQ/riscv-formal) framework, developed by Claire Wolf (YosysHQ).