Skip to content

cliffordwolf/riscv-formal

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

RISC-V Formal Verification Framework

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

About

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 the RISC-V Formal Interface (RVFI) that must be implemented by a processor core to interface with riscv-formal.
  • Some auxiliary proofs and scripts, for example to prove correctness of the ISA spec agains riscv-isa-sim.

See cores/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.

Table of contents

Configuring a new RISC-V processor

  1. Create a riscv-formal/cores/<core-name>/ directory
  2. Write a wrapper module that instantiates the core under test and abstracts models of necessary peripherals (usually just memory)
  3. Write a checks.cfg config file for the new core
  4. Generate checks with python3 ../../checks/genchecks.py from the <core-name> directory
    • Checks are generated in riscv-formal/cores/<core-name>/checks
  5. Run checks with make -C checks j$(nproc)

Notes

  • The quickstart guide goes through the process of running riscv-formal with some of the included cores. It is recommended to follow this guide before adding a new core.
  • See picorv32/Makefile for an example makefile to manage generation and execution of checks.
  • Out of tree generation with genchecks.py is not currently supported.
  • Refer to docs/config.md and docs/procedure.md for a breakdown of how to use riscv-formal checks without using genchecks.py.
  • The cover check can be used to help determine the depth needed for the core to reach certain states as needed for other checks.

About

RISC-V Formal Verification Framework

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • Verilog 54.4%
  • SystemVerilog 38.6%
  • Python 5.6%
  • Shell 0.5%
  • C++ 0.3%
  • Makefile 0.3%
  • Other 0.3%