# rvsail
Formal verification of RISC-V processors using the [Sail ISA model](https://github.com/rems-project/sail-riscv) 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.
## 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](https://github.com/YosysHQ/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](https://github.com/coruus/canright-aes-sboxes/issues/2) | Undriven wire in GF_INV_4 | Unnoticed for 12 years. Combinational check. |
| [croyde-riscv](https://github.com/ben-marshall/croyde-riscv/issues/4) | Barrel shifter bit-reversal index | Left shifts (SLL/SLLI/SLLW) produce wrong bit 0. BMC check. |
## Install
```bash
# Combinational checks (Rust CLI)
cargo install rvsail
# Sequential BMC (requires Yosys + SymbiYosys + solver)
# See software/rvfi/rvfi_check.sh --help
```
Prerequisites: [Yosys](https://github.com/YosysHQ/yosys), [Z3](https://github.com/Z3Prover/z3) (or [Boolector](https://github.com/Boolector/boolector)), [SymbiYosys](https://github.com/YosysHQ/sby) (for BMC).
## Quick start
```bash
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
```bibtex
@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