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.

Live Dashboard | crates.io

What it does

rvsail checks that a RISC-V RTL implementation matches the official ISA specification — automatically. It uses the 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

cargo install rvsail

You also need Yosys and Z3:

# macOS
brew install yosys z3

# Ubuntu/Debian
sudo apt install yosys z3

# Arch
sudo pacman -S yosys z3

Quick start

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

Total: 222/223 verified, 1 real bug found (coruus/canright-aes-sboxes#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:

[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:

rvsail verify my_alu.toml

Bug found

rvsail discovered a real bug in the Canright AES S-box — 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.

License

MIT