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/rvsail
cd rvsail

# Verify a named bridge group (resolves to all manifests for that target)
rvsail verify --bridge vicuna    # Vicuna vector ALU + MUL (50 ops)
rvsail verify --bridge crypto    # RISC-V Crypto AES32 + SHA256 (20 ops)

# Verify individual manifests (still works)
rvsail verify software/bridges/crypto_aes32.toml

# Run the S-box sweep across multiple RTL targets
rvsail sweep                              # all sweep targets
rvsail sweep --bridge crypto              # crypto S-box targets
rvsail sweep --targets secworks,canright  # specific targets

# 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.

Experiments (deprecated)

The experiments/ directory contains legacy Python verification scripts that have been consolidated into the Rust CLI. These scripts are preserved for reference but should not be used for new work:

• experiments/vicuna_bridge/ — use rvsail verify --bridge vicuna instead
• experiments/crypto_bridge/ — use rvsail verify --bridge crypto instead
• experiments/crypto_bridge/sweep_sbox.py — use rvsail sweep instead

License

MIT