# rvsail
Formal verification of RISC-V processors using the Sail ISA model as an automatic oracle.
One command. Zero hand-written properties. 222 ops verified across 19 RTL targets.
## What it does
rvsail checks that a RISC-V RTL implementation matches the official ISA specification — automatically. It uses the [Sail](https://github.com/rems-project/sail) ISA model as a golden oracle, so you don't need to write any properties by hand.
```
$ rvsail verify bridges/crypto_sha256.toml
RVS Bridge: crypto_sha256
RISC-V Crypto SHA256 (Zknh) -- rotation/shift ops
[Yosys] Flattening RTL to SMT2... Done (32ms)
[Z3] Checking 4 operations...
+ sha256sig0 UNSAT 17ms
+ sha256sig1 UNSAT 16ms
+ sha256sum0 UNSAT 16ms
+ sha256sum1 UNSAT 17ms
PASS: crypto_sha256 -- 4/4 UNSAT (68ms)
```
## Install
```bash
cargo install rvsail
```
You also need [Yosys](https://github.com/YosysHQ/yosys) and [Z3](https://github.com/Z3Prover/z3):
```bash
# macOS
brew install yosys z3
# Ubuntu/Debian
sudo apt install yosys z3
# Arch
sudo pacman -S yosys z3
```
## Quick start
```bash
git clone https://github.com/yiidtw/rvs
cd rvs
# Verify RISC-V crypto instructions (20 ops, ~40s)
rvsail verify software/bridges/crypto_aes32.toml
rvsail verify software/bridges/crypto_sha256.toml
# Verify Vicuna vector ALU (44 ops, ~2s)
rvsail verify software/bridges/vicuna_alu.toml
# Detect a known bug in Canright AES S-box (expects SAT)
rvsail verify software/bridges/sweep_canright.toml
```
## Verified targets
| CVA6/Ariane ALU | RV64I | 15 | UNSAT |
| BOOM ALU | RV64I+Zbb | 15 | UNSAT |
| Rocket ALU | RV64I+Zbb | 18 | UNSAT |
| Xiangshan ALU | RV64I+Zba+Zbb+Zbs | 29 | UNSAT |
| IBEX ALU | RV32I | 10 | UNSAT |
| CV32E40P ALU | RV32I | 10 | UNSAT |
| PicoRV32 ALU | RV32I | 10 | UNSAT |
| SERV ALU | RV32I | 10 | UNSAT |
| SweRV ALU | RV32I | 10 | UNSAT |
| riscv-mini ALU | RV32I | 10 | UNSAT |
| Vicuna Vector ALU | RV32V | 44 | UNSAT |
| Vicuna Vector MUL | RV32V | 6 | UNSAT |
| RISC-V Crypto AES32 | RV32Zkn | 16 | UNSAT |
| RISC-V Crypto SHA256 | RV32Zknh | 4 | UNSAT |
| secworks AES S-box | AES | 1 | UNSAT |
| **Canright AES S-box** | **AES** | **1** | **SAT (bug found)** |
**Total: 222/223 verified, 1 real bug found** ([coruus/canright-aes-sboxes#2](https://github.com/coruus/canright-aes-sboxes/issues/2))
## How it works
```
Verilog RTL ──→ Yosys ──→ SMT2 ──┐
├──→ Z3 ──→ UNSAT (equivalent)
Sail ISA model ──→ Oracle ────────┘ or SAT (bug found)
```
1. **Yosys** flattens your Verilog/SystemVerilog to an SMT2 model
2. The **Sail ISA oracle** provides the expected behavior (zero manual effort)
3. **Z3** checks equivalence: UNSAT = your RTL matches the spec
Each verification target is defined by a TOML manifest — add your own core in minutes.
## Adding a new target
Create a TOML manifest:
```toml
[target]
name = "my_alu"
description = "My custom RISC-V ALU"
[rtl]
files = ["path/to/alu.v"]
top_module = "alu"
yosys_commands = "prep -top alu; write_smt2 -wires {output}"
[verify]
z3_timeout = 60
[[ops]]
name = "add"
spec_file = "specs/add_spec.smt2"
constraints_file = "specs/add_constraints.smt2"
assert_neq = "(assert (not (= rtl_out spec_out)))"
```
Then run:
```bash
rvsail verify my_alu.toml
```
## Bug found
rvsail discovered a real bug in the [Canright AES S-box](https://github.com/coruus/canright-aes-sboxes) — an undriven wire in `GF_INV_4` that went unnoticed for 12 years. The bug was confirmed and reported upstream: [coruus/canright-aes-sboxes#2](https://github.com/coruus/canright-aes-sboxes/issues/2).
## License
MIT