χRVFormal

χRVFormal is a formal verification framework for validating the instruction-level correctness of RISC-V processors implemented in Chisel.

It provides:

A configurable reference model (RiscvCore) that encodes the RISC-V ISA semantics
A set of checkers and helpers to connect your DUT with the reference model
Built-in formal properties for ISA consistency checking

Read more detailed Chinese README: 中文说明.

χRVFormal

✨ Features

✅ Supports RV32/RV64 I
✅ ISA extensions: M, B, C, Zicsr, Zifencei
✅ Privilege modes: M, S, U
✅ Virtual memory with Sv39
✅ Reg/ Memory / CSR / TLB consistency checking
✅ Works with ChiselTest + BMC (BtorMC)
✅ Optional Verilog flow (SymbiYosys)

🚀 Quick Start

1. Add Dependency

Option A: Local build (recommended)

git clone https://github.com/iscas-tis/ChiRVFormal.git
cd ChiRVFormal
sbt publishLocal -DHashId=true

Then in your build.sbt:

libraryDependencies += "cn.ac.ios.tis" %% "riscvspeccore" % "<your-version>"

Option B: SNAPSHOT from Maven

resolvers += Resolver.sonatypeRepo("snapshots")
libraryDependencies += "cn.ac.ios.tis" %% "riscvspeccore" % "1.3-SNAPSHOT"

🧩 Usage

Step 1 — Instantiate the Checker

val rvConfig = RVConfig(
  XLEN = 64,
  extensions = "MCZicsrU",
  fakeExtensions = "A",
  initValue = Map("pc" -> "h0000_8000"),
  functions = Seq("Privileged", "TLB"),
  formal = Seq("CheckMem", "CheckCSRs")
)

val checker = Module(new CheckerWithState(enableReg = false)(rvConfig))

Step 2 — Connect Commit Signals

Hook your pipeline commit stage:

checker.io.instCommit.valid := commit_valid
checker.io.instCommit.excp  := commit_excp
checker.io.instCommit.inst  := commit_inst
checker.io.instCommit.pc    := commit_pc
checker.io.instCommit.npc   := commit_npc

Initialize helper:

ConnectHelper.setChecker(checker)(XLEN, rvConfig)

Step 3 — Provide Architectural State

General Register

val regStateWire = Wire(Vec(32, UInt(XLEN.W)))
regStateWire := rf
regStateWire(0) := 0.U
ConnectHelper.setRegSource(regStateWire)

Privilege State

val privilegeStateWire = ConnectHelper.makePrivilegeSource(rvConfig)
// cur priviledge mode
privilegeStateWire.mode          := RegNext(priviledgeMode)
// csrs
privilegeStateWire.csr.mvendorid := RegNext(mvendorid)
privilegeStateWire.csr.marchid   := RegNext(marchid)
// ······

TLB

Get signals in TLB of DUT.

val tlbAccessWrie = ConnectHelper.makeTLBSource(if(tlbname == "itlb") false else true)(XLEN)
// memory access in TLB
resultTLBWire.read.valid := true.B
resultTLBWire.read.addr  := io.mem.req.bits.addr
resultTLBWire.read.data  := io.mem.resp.bits.rdata
resultTLBWire.read.level := (level-1.U)
// ······

Memory Access

Get the signal when DUT access memory.

val memAccessWire = ConnectHelper.makeMemSource()(XLEN)
memAccessWire.read.valid      := isRead
memAccessWire.read.addr       := addr
memAccessWire.read.data       := backend.io.dmem.resp.bits.rdata
memAccessWire.read.memWidth   := width

memAccessWire.write.valid     := isWrite
memAccessWire.write.addr      := addr
memAccessWire.write.data      := wdata
memAccessWire.write.memWidth  := width

Step 4 — Add Constraints

Use assume to restrict the input space:

assume(RVI(inst))
assume(RVI.ADDI(inst))

Step 5 — Run Formal Verification

verify(new DUT(), Seq(
  BoundedCheck(12),
  BtormcEngineAnnotation
))

⚡ Single Instruction Mode

Speed up debugging by focusing on one instruction:

val checker = Module(
  new CheckerWithState(singleInstMode = Some(RVI.ADDI))(rvConfig)
)

🔌 Verilog Flow (Optional)

1. Configure model by JSON

{
  "xlen": 32,
  "extensions": ["I", "Zicsr", "Zba", "Zbb", "Zbc", "Zbs", "Zbkb", "Zbkc", "Zbkx"],
  "fakeExtensions": [],
  "initValue": {"pc": "h8000_0000", "mstatus": "h0000_1800", "mtvec": "h0000_0000"},
  "functions": ["Privileged"],
  "formal": ["CheckMem", "CheckNPC", "CheckCSRs"],
  "regDelay": false,
  "singleInstMode": null
}

2. Generate SystemVerilog

> sbt "svcore/runMain svcore.Main -h"
[info] running svcore.Main -h
SystemVerilog Spec Core Generator 1.3
Usage: sv-cores [options]

  -c, --config <file>      path to the configuration file (default: config.json)
  -m, --model <model>      check model to generate (default: writeback)
  -t, --target-dir <directory>
                           directory to output the generated SystemVerilog files (default: build)
  -l, --list               show list of supported models
  -h, --help               show list of command-line options

3. Run SymbiYosys

config SymbiYosys by formal.sby

[options]
mode bmc
expect pass,fail
append 0
depth 16
skip 15

[engines]
smtbmc boolector

[script]
read -sv testbench.sv
prep -flatten -nordff -top testbench
chformal -early

[files]
testbench.sv

run command:

sby -f formal.sby

💡 Tips

Use SingleInstMode first when debugging failures
Add minimal assume constraints to avoid state explosion
Run formal checks in CI (GitHub Actions) to catch regressions early

📂 Examples

NutShell integration: nutshell-fv
SystemVerilog/Verilog examples: sv-core-fv

📄 Publications

If this project is useful in your research, please cite:

SETTA 2024: Formal Verification of RISC-V Processor Chisel Designs Link | BibTex

JSA 2026: χRVFormal: Formal Verification of RISC-V Processor Chisel Designs Link | BibTex

iscas-tis / chirvformal 1.0.0