ExaVerif

Exhaustive Verification for RISC‑V Custom Instructions

Author

Affiliation

SSCCS Foundation

SSCCS Foundation

Abstract

ExaVerif performs exhaustive verification of RISC‑V custom instruction extensions. A YAML file describing a module’s constraints is all that is required — ExaVerif generates every valid constraint combination, evaluates each one deterministically, and produces an auditable report with optional LLM‑powered interpretation. It is distributed under an open‑core model: the CLI is free and open‑source, while advanced interpretation, collaboration, and formal certification are available through paid tiers.

Code

Github

Other Formats

LLMs

The Problem

RISC‑V’s defining advantage is its extensibility. Custom instruction extensions (XIF) enable domain‑specific acceleration for AI inference, signal processing, cryptography, and embedded control. Every custom instruction must be verified across its full operational envelope — operand ranges, pipeline states, data alignment, hazard conditions, and physical constraints.

The current verification tooling faces two persistent obstacles:

1. No automated constraint composition. Random instruction generators produce statistical coverage but cannot enumerate the complete space of interacting constraints. When operand ranges, pipeline depth, and alignment rules combine, the number of valid configurations reaches into the thousands. Manual test writing cannot scale to cover this space exhaustively.
2. Non‑deterministic coverage. Random‑seed‑based simulation cannot determinically prove that a specific edge case was tested. Reproducing a failure requires preserving the exact seed, environment state, and tool versions — a fragile chain that breaks across teams and over time.

What ExaVerif Does

ExaVerif replaces random sampling with deterministic constraint composition. A developer describes the module’s constraints in a YAML file. A single command generates every valid constraint combination, evaluates each one, and produces a complete pass/fail report.

ev check --target my_xif.yaml
ev check --target my_xif.yaml --interpret
ev certify --target my_xif.yaml --output certificate.pdf

Internally, ExaVerif uses the Field Composition engine — a branchless, constant‑time verification kernel that has been internally validated via x86‑64 CI — to guarantee that every evaluation is deterministic. The same input always produces the same result, independent of random seeds or simulator state.

The optional --interpret flag runs a lightweight LLM pass over failures and explains why each one occurred. All results are committed as immutable Fact records to the shared blackboard — a verifiable, append‑only knowledge store shared across the RISC‑V verification ecosystem. Once committed, these facts become reusable verification knowledge for any project.

Why ExaVerif Is Different

	Existing Tools	ExaVerif
Coverage	Random sampling, manual test writing	Exhaustive constraint combination
Evaluation	Seed‑dependent, simulator‑dependent	Deterministic
Setup	UVM/SystemVerilog environment, commercial simulators	Single YAML file, single binary
Interpretation	Manual log analysis	LLM‑powered natural‑language explanation
Result reuse	One‑time reports	All facts accumulated on shared blackboard

Figure 1: ExaVerif fills the unfilled quadrant: exhaustive coverage combined with zero‑setup CLI accessibility.

Business Model

ExaVerif is distributed under an open‑core model. The CLI is open‑source (Apache 2.0) and free to use. Paid tiers provide advanced interpretation, collaboration features, and formal certification.

Tier	Price	Scope
ExaVerif CLI	Free (Apache 2.0)	ExaVerif check — basic composition and evaluation
ExaVerif Pro	draft	--interpret LLM analysis, history, blackboard access
ExaVerif Enterprise	draft	Custom constraint templates, CI/CD integration, SLA
ExaVerif Certification	draft	Signed verification certificate with on‑chain proof

Certification pricing reflects the complexity of the module under verification — a single‑cycle integer XIF with two operands sits at the lower bound; a multi‑cycle vector accelerator with pipeline interactions and physical constraints sits at the upper bound. Each engagement produces a cryptographically signed audit report and, optionally, an on‑chain proof of verification.

Market Context

Figure 2: RISC-V Technology Market Size Forecast (2025–2031)

Figure 3: Global EDA and Verification Market Size Forecast (2025–2031)

The RISC‑V technology market is projected to grow from $1.35B in 2025 to $10.7B by 2031 at a 41.2% CAGR. Verification accounts for roughly 30% of the broader EDA market, which reached $19.22B in 2025. Custom instruction extensions are a primary driver of RISC‑V adoption, and every custom instruction requires verification that existing tools cannot exhaustively provide.

Competitive Landscape

Tool	Approach	Limitation
RISCV‑DV	Constrained‑random instruction generation	Statistical coverage; misses deterministic edge cases
Breker SystemVIP	AI‑assisted test synthesis	Random seed‑based; commercial license required
ImperasDV	Simulation‑based verification with RVVI	Requires commercial simulator; manual test writing
VC Formal / Axiomise	Formal property verification	Complex setup; verifies specific properties only
RiESCUE	Directed compliance testing	Limited to specific extensions; no combination generation

No existing tool performs exhaustive constraint composition. ExaVerif addresses this gap by generating every valid constraint combination and evaluating each deterministically.

Collaboration with the Ecosystem

ExaVerif is being developed as an independent product within the RISC‑V ecosystem. It is not tied to any single organization, core, or workflow. The project welcomes collaboration with groups working on RISC‑V verification — including OpenHW, PULP, and individual core developers — to validate the approach against real‑world custom instruction extensions and to integrate ExaVerif’s deterministic constraint composition into existing verification workflows.

Collaboration is structured as a mutual exchange: partners provide domain expertise and access to real‑world XIF designs for validation; the ExaVerif project provides the tool, methodology, and certification infrastructure. All verification facts generated through collaboration are deposited on the shared blackboard, where they become reusable knowledge for the entire ecosystem.

Connection to the Substrate

ExaVerif is an independent domain entity built on the shared substrate — a working demonstration of the model described in the Project Model. Every verification run feeds the shared blackboard. A failure pattern discovered in one module becomes a hint for every other RISC‑V project. The product earns revenue; the substrate earns knowledge.