rvsail

Formal verification of RISC-V processors using the Sail ISA model as an automatic oracle.

Zero hand-written properties. From combinational ALU checks to sequential bounded model checking with decomposed Burch-Dill proofs across 5 RISC-V cores.

Docs | crates.io |

What it does

rvsail checks that RISC-V hardware matches the official ISA specification — automatically. It extracts verification conditions from the Sail formal model, so you write zero properties by hand.

Two levels of verification:

Level 1 — Combinational equivalence (rvsail verify): instant per-operation checks against Sail-derived SMT oracles.

$ rvsail verify --bridge crypto
  + aes32esmi              UNSAT        23ms
  + sha256sig0             UNSAT        17ms
  ...
PASS: 20/20 UNSAT (312ms)

Level 2 — Sequential BMC (rvfi_check.sh): bounded model checking of full processor cores via riscv-formal, using Sail-derived instruction checkers + Burch-Dill monitor proofs.

$ ./software/rvfi/rvfi_check.sh croyde --solver boolector
  --- [croyde] insn_add ---
  DONE (PASS, rc=0)                     28s
  --- [croyde] insn_sub ---
  DONE (PASS, rc=0)                     55s
  ...
  21/24 PASS, 3 FAIL (sll/slli/sllw — barrel shifter issue)

Results

Sequential BMC — 5 cores, 185 checks

Core	ISA	Insn Checks	Sequential	Burch-Dill Monitor	Solver
NERV	RV32I	37/37	3/3	5/5	z3
PicoRV32	RV32IMC	37/37	2/2	10/10	z3
SERV	RV32I	37/37	2/2	12/12	z3
Ibex	RV32IMC	37/37	2/2	8/8	z3
croyde	RV64I	21/24	2/2	4/4	boolector

The decomposed Burch-Dill proof completes the trust chain for each core:

Sail ISA spec  <── insn checks ──>  RVFI  <── monitor ──>  actual RTL

Combinational — 222 ops across 19 targets

Target	ISA	Ops	Result
Xiangshan ALU	RV64I+Zba+Zbb+Zbs	29	UNSAT
Rocket ALU	RV64I+Zbb	18	UNSAT
BOOM ALU	RV64I+Zbb	15	UNSAT
CVA6/Ariane ALU	RV64I	15	UNSAT
Vicuna Vector ALU	RV32V	44	UNSAT
RISC-V Crypto AES32	RV32Zkn	16	UNSAT
...	...	...	...
Canright AES S-box	AES	1	SAT

222/223 verified, 2 real issues found in external projects.

Issues found

Project	Issue	Description
Canright AES S-box	Undriven wire in GF_INV_4	Unnoticed for 12 years. Combinational check.
croyde-riscv	Barrel shifter bit-reversal index	Left shifts (SLL/SLLI/SLLW) produce wrong bit 0. BMC check.

Install

# Combinational checks (Rust CLI)
cargo install rvsail

# Sequential BMC (requires Yosys + SymbiYosys + solver)
# See software/rvfi/rvfi_check.sh --help

Prerequisites: Yosys, Z3 (or Boolector), SymbiYosys (for BMC).

Quick start

git clone https://github.com/yiidtw/rvsail && cd rvsail

# Combinational: verify an ALU
rvsail verify --bridge vicuna        # Vicuna vector ALU (50 ops)
rvsail verify --bridge crypto        # RISC-V Crypto (20 ops)

# Sequential BMC: verify a processor core
cd software/rvfi
./rvfi_check.sh nerv                 # NERV full sweep (37 insns, ~1h)
./rvfi_check.sh croyde --solver boolector  # croyde RV64I (~14 min)
./rvfi_check.sh --help               # all cores and options

# Regression suite
./regression.sh --quick              # smoke test (14 checks, ~30 min)
./regression.sh                      # full suite (185 checks, ~2h)

How it works

                    ┌─────────────┐
                    │  Sail ISA   │  (official RISC-V formal spec)
                    │    Model    │
                    └──────┬──────┘
                           │ Isla symbolic execution
                    ┌──────┴──────┐
              ┌─────┤  SMT traces │─────┐
              │     └─────────────┘     │
              ▼                         ▼
    ┌──────────────────┐    ┌──────────────────┐
    │  L1: Combinational│    │  L2: Sequential  │
    │  rvsail verify    │    │  rvfi_check.sh   │
    │  (Yosys + Z3)     │    │  (SymbiYosys BMC)│
    │  222 ops, 19 ALUs │    │  5 cores, 77 chks│
    └──────────────────┘    └──────────────────┘

Project structure

rvsail/
├── software/
│   ├── src/              # Rust CLI (rvsail verify, sweep)
│   ├── bridges/          # TOML manifests for combinational checks
│   ├── specs/            # Sail-derived SMT2 specs
│   └── rvfi/             # Sequential BMC infrastructure
│       ├── rvfi_check.sh # Unified entry point
│       ├── cores/        # Per-core configs (nerv, ibex, croyde, ...)
│       ├── lib/          # Shared BMC library
│       ├── insns/        # RV32I Isla checkers (37)
│       ├── insns64/      # RV64I Isla checkers (24)
│       ├── monitors/     # Burch-Dill monitor wrappers
│       └── regression.sh # 77-check regression suite
├── docs/site/            # mdbook (GitHub Pages)
└── extern/               # Third-party RTL (Ibex, SERV, ...)

Citation

@software{rvsail2026,
  title  = {rvsail: RISC-V Formal Verification via Sail ISA Oracle},
  author = {YD Wu},
  year   = {2026},
  url    = {https://github.com/yiidtw/rvsail},
  doi    = {10.5281/zenodo.19163880},
}

License

MIT

rvsail 0.15.0