Formal verification tools for Chisel and RISC-V.
A verification tool that supports SVA-like assertions in Chisel.
CHA is an assertion language and verification tool for Chisel programs built on top of ChiselTest, where we extend the Chisel assertion language with SystemVerilog assertions (SVA)-like temporal operators. This enables formal verification of Chisel hardware designs against general temporal properties.
SEFM 2022: CHA: Supporting SVA-Like Assertions in Formal Verification of Chisel Programs (Tool Paper) Link | BibTex
Instruction set consistency verification for RISC-V.
ChiRVFormal uses a reference model as the formal semantics of the RISC-V ISA document. The Chisel processor design to be verified should behave the same as the reference model. This project also includes tools for signal synchronization between the reference model and the processor design.
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
A two-way hybrid verification approach that synergistically integrates bounded model checking and coverage-guided fuzzing.
BMCFuzz is a fuzzing framework for processor verification that combines bounded model checking (BMC) and coverage-guided fuzzing (CGF). BMC and CGF are complementary: BMC is exhaustive within a bound but suffers from state-space explosion, while CGF is scalable but seed-dependent. BMCFuzz integrates both in a two-way workflow and is evaluated on NutShell, Rocket, and BOOM, reporting higher coverage and three previously unknown vulnerabilities.
ICCAD 2025: BMCFuzz: Hybrid Verification of Processors by Synergistic Integration of Bound Model Checking and Fuzzing Link
Formally verifying the FIRRTL compilation flow in Coq.
Coq-firrtl formalizes and proves
the correctness of three key FIRRTL compilation steps.
It also improves the width inference algorithm in the official compiler
firtool by proposing a complete procedure, together with its implementation
and mechanized correctness proof.
ESOP 2026: A Formally Verified Procedure for Width Inference in FIRRTL
A high-level Chisel verification method based on Chisel-to-Scala translation and Stainless.
Chicala translates Chisel hardware designs into Scala programs via a compiler plugin, enabling deductive verification with Scala software verification tool Stainless. It supports reasoning with Chisel-level parameter and structure information, including proofs for arithmetic designs across bit widths.
DAC 2024: Formally Verifying Arithmetic Chisel Designs for All Bit Widths at Once Link | BibTex
A neuro-symbolic approach for solving constraints with inductive definitions.
LLM4Ind is a project on leveraging large language models to help solve constraints involving inductive (recursive) definitions. It uses structured prompts to generate auxiliary lemmas, then iteratively combines LLM conjecture generation with SMT solver checking in a neuro-symbolic loop. On benchmarks from algebraic data types and recurrence relations, it reports around 25% more solved proof tasks than state-of-the-art SMT/CHC solvers.
FM 2026: Can LLM Aid in Solving Constraints with Inductive Definitions?