Welcome to the RISC-V Formal Verification Framework documentation!

riscv-formal is a framework for formal verification of RISC-V processors. This framework is built around the RISC-V Formal Interface (RVFI), providing a set of formal testbenches utilizing SystemVerilog Assertions (SVA). These can be used to verify behaviour on this interface, and by extension prove functional correctness of a RISC-V processor. Tests can be generated for SBY automatically with the included Python scripts or used as-is.

Contents:

• Quick start guide
  • Prerequisites
  • Exercise 1: Formally verify a core
  • Exercise 2: Build an RVFI Monitor and run it
• RISC-V Formal Interface (RVFI)
  • RVFI specification
  • RVFI TODOs and requests for comments
• CSR semantics
  • M-mode CSRs
  • Debug-Mode CSRs
  • U-Mode CSRs
  • S-Mode CSRs
• Defining macros
  • Configuration macros
  • Testbench macros
  • Macros defined by rvfi_macros.vh
• Verification procedure
  • Configuring check generation
  • Standard checks
  • Standard bus checks
  • CSR checks
  • Other checks
• Examples of bugs found by RISC-V Formal
  • Instruction semantics
  • Troubles with bypassing and forwarding
  • Issues with reset
  • Weird and bizarre programs
• References and related work