riscv-formal Flow

This flow is the principle way that instruction implementations are verified.

It uses the riscv-formal framework.

Note that this flow checks only user-level instruction behaviours. It does not check privilidged architecture operations or interractions.

Running the flow:

make riscv-formal-clean
make riscv-formal-prepare
make riscv-formal-run

By default the flow will run $(nproc) checks in parallel. This can be tuned by specifying the RV_FORMAL_NJOBS=X makefile parameter explicitly.

A single proof may be re-run with the following commands:

make riscv-formal-clean
make riscv-formal-prepare
sby -f work/riscv-formal/[proof name].sby

Flow outputs:

  • All flow outputs are placed in work/riscv-formal

  • Each directory corresponds to the output of a single check.

Relevant files:

  • See verif/riscv-formal for project specific files.

  • rvfi_wrapper.sv wraps the core and exposes the formal verification interface (RVFI) signals. It also instantiates any fairness assumption blocks.

  • rvfi_fairness.sv contains assumptions which make the formal engines "play fair`. These include maximum stall lengths and constrains on how the externally driven memory interface signals behave.