Skip to content
RISC-V Formal Verification Framework
Verilog Python SystemVerilog Other
Branch: master
Clone or download
cliffordwolf Rocket renamed rocket_tile.RVFI_csr_instret_* to rocket_tile.RVFI_csr…
…_minstret_*

Signed-off-by: Clifford Wolf <clifford@clifford.at>
Latest commit 82a34fa Aug 20, 2019
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
checks Another fix in CSR handling Aug 20, 2019
cores Rocket renamed rocket_tile.RVFI_csr_instret_* to rocket_tile.RVFI_csr… Aug 20, 2019
docs Add RISCV_FORMAL_ALTOPS to config.md Aug 7, 2019
insns Add corner cases to div/rem instructions, fixes #29 Aug 7, 2019
monitor Fix monitor/generate.py to support macros besides RISCV_FORMAL_COMPRE… Nov 5, 2018
tests
.gitignore testbug support in picorv32 example Jul 1, 2019
COPYING Update copying email address Aug 9, 2018
CodeOfConduct Add CodeOfConduct Nov 10, 2017
README.md Add RISC-V Formal CSR Sematics Aug 17, 2018

README.md

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

See also this presentation slides for an introduction to riscv-formal.

You can’t perform that action at this time.