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:
riscv-formal
.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.
riscv-formal/cores/<core-name>/
directoryRVFI_OUTPUTS
and RVFI_CONN
for quickly defining wrapper connectionschecks.cfg
config file for the new core
genchecks.py
python3 ../../checks/genchecks.py
from the <core-name>
directory
riscv-formal/cores/<core-name>/checks
make -C checks j$(nproc)
genchecks.py
is not currently supported.genchecks.py
.