Repository files navigation

This is work in progress. The interfaces described here are likely to change as the project matures.

riscv-formal is a framework for formal verification of RISC-V processors.

It consists of the following components:

• A processor-independent formal description of the RISC-V ISA
• A set of formal testbenches for each processor supported by the framework
• The specification for theRISC-V Formal Interface (RVFI) that must be implemented by a processor core to interface withriscv-formal.
• Some auxiliary proofs and scripts, for example to prove correctness of the ISA spec agains riscv-isa-sim.

Seecores/picorv32/ for example bindings for the PicoRV32 processor core.

A processor core usually will implement RVFI as an optional feature that is only enabled for verification. Sequential equivalence check can be used to prove equivalence of the processor versions with and without RVFI.

The current focus is on implementing formal models of all instructions from the RISC-V RV32I and RV64I ISAs, and formally verifying those models against the models used in the RISC-V "Spike" ISA simulator.

riscv-formal uses the FOSS SymbiYosys formal verification flow. All properties are expressed using immediate assertions/assumptions for maximal compatibility with other tools.

• Quickstart Guide
• The RVFI Interface Specification
• RISC-V Formal CSR Sematics
• Configuration macros used by riscv-formal
• The riscv-formal Verification Procedure
• Examples of bugs found with riscv-formal
• References and related work

1. Create ariscv-formal/cores/<core-name>/ directory
2. Write a wrapper module that instantiates the core under test and abstracts models of necessaryperipherals (usually just memory)
   • Use theRVFI helper macrosRVFI_OUTPUTS andRVFI_CONN for quickly defining wrapper connections
   • Seepicorv32/wrapper.sv for a simple example wrapper
3. Write achecks.cfg config file for the new core
   • Seenerv/checks.cfg for an example utilising most of the checks
   • Refer toThe riscv-formal Verification Procedure for a complete guide onavailable checks, and a more detailed view of usinggenchecks.py
4. Generate checks withpython3 ../../checks/genchecks.py from the<core-name> directory
   • Checks are generated inriscv-formal/cores/<core-name>/checks
5. Run checks withmake -C checks j$(nproc)

• Thequickstart guide goes through the process of running riscv-formal withsome of the included cores. It is recommended to follow this guide before adding a new core.
• Seepicorv32/Makefile for an example makefile to manage generation andexecution of checks.
• Out of tree generation withgenchecks.py is not currently supported.
• Refer todocs/config.md anddocs/procedure.md for abreakdown of how to use riscv-formal checks without usinggenchecks.py.
• Thecover check can be used to help determine the depth needed for thecore to reach certain states as needed for other checks.