ExaVerif

Exhaustive Verification for RISC‑V Custom Instructions

Author
Affiliation

SSCCS Foundation

SSCCS Foundation

Published

June 4, 2026

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. The CLI is open‑source (Apache 2.0). The engine is validated against the CVA6 CV-X-IF reference coprocessor (33.5 million combinations, 32 seconds), with cross‑verification through Spike RISC-V simulation.

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 treats a YAML description as a Spec Space: field domains define its axes, constraints carve admissible subspaces, and each combination is a point within this space. A single command enumerates and evaluates every point exhaustively.

ev verify --target cva6_xif_ref.xif.yaml

Internally, ExaVerif expands the full cartesian product of all field domains, then evaluates each combination against every declared constraint. The result is exact: every passing combination is a valid instruction encoding; every failing combination has a specific, recorded reason.

target: cva6_xif_ref
total:  33554432
passed: 196608
failed: 33357824

The example above shows ev verifying the CVA6 CV-X-IF reference coprocessor against its actual RTL specification — the same encoding tables used in the CVA6 verification suite (cvxif_custom_instr.sv). Over 33 million raw combinations are evaluated exhaustively. Only 196,608 encodings are valid: every funct3/funct7 combination that the coprocessor actually accepts, with full RV32 register range (rs1, rs2, rd ∈ [0, 31]). The remaining 33 million are correctly identified as illegal.

ev verify --target cva6_xif_ref.xif.yaml --json

Every result is also available as a Fact — an opaque blob consumed by Nexus. Each combination becomes a point in the spec space, each constraint a boundary, and the verification run itself an Intent. No schema is embedded at the transport layer; consumers interpret the payload based on its fact_type discriminator.

EV_SIM_BACKEND=spike ev simulate --target cva6_xif_ref.xif.yaml

Every valid encoding is also verifiable through actual RISC-V simulation. The simulate command packs all 196,608 valid encodings into a single ELF binary, runs it under Spike + pk on RV64, and reports the result. All 196,608 pass — the static constraint model and the RISC-V simulator agree exactly.

The Field Composition engine — a branchless, constant‑time verification kernel validated via x86‑64 CI — guarantees deterministic results. The same input always produces the same output, independent of random seeds or simulator state.

Figure 1: ExaVerif verification results flow into Nexus’s knowledge base; the same FIH cycle operates inside ExaVerif itself.

ExaVerif’s verification results are consumed by Nexus, the autonomous research infrastructure. The same FIH cycle operates inside ExaVerif itself at a different scale — domain expansion as Intent, each evaluated combination as a Fact, each constraint as a Hint — making ExaVerif a Nexus instance in its own right. Every constraint combination evaluated, every failure pattern discovered, and every coverage gap identified flows into Nexus’s knowledge base, where it becomes training material for the agentic research loop and reusable knowledge for the entire RISC‑V ecosystem.

How the Industry Verifies Custom Instructions

Approach Representative Tools Coverage Limitation
Random simulation RISCV‑DV, Breker Statistical, seed‑based Misses deterministic edge cases
Formal verification OneSpin, Axiomise Per‑property proofs Complex setup; capacity limits
Reference model ImperasDV Simulation‑bound lockstep Model may contain blind spots
Compliance testing RISC‑V ACT, RISCOF Architectural conformance No custom extension coverage

Every approach shares one trait: coverage is either statistical or scoped to specific properties. None enumerates every valid constraint combination and evaluates each deterministically.

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 Deterministic reason output (LLM explanation planned)
Result reuse One‑time reports All results accumulated as reusable knowledge

Benchmark: CVA6 XIF Reference Coprocessor

A single ev verify command exhaustively evaluates 33.5 million raw field combinations against the actual CVA6 CV-X-IF encoding specification. The coprocessor accepts 196,608 valid encodings — the exact funct3/funct7/rs1/rs2/rd combinations that match its decoder — and correctly rejects the remaining 33.3 million. Execution time on a laptop (Apple M1 Max, single core): 32 seconds. All 196,608 valid encodings are independently confirmed through RISC-V ISA simulation (Spike) with exact agreement.

Metric RISC-V DV (random) Formal (OneSpin) ExaVerif
Combos evaluated ~10⁶ (sampled) ~10³ (properties) 33.5 × 10⁶ (exhaustive)
Coverage guarantee Statistical Formal (per property) Exhaustive (full space)
Time to result Minutes to hours Hours to days 32 seconds
Setup UVM env. + agent Formal properties Single YAML
Cross-validated — — Spike simulation ✓
Figure 2: ExaVerif fills the unfilled quadrant: exhaustive coverage combined with zero‑setup CLI accessibility.

Automated Issue Management

Verification results feed into the shared knowledge store (Nexus), where they become permanent, queryable records. A failure analyzed once never needs diagnosis from scratch again.

Acknowledging the Limits of Exhaustive Verification

Exhaustive verification carries an inherent constraint: the number of combinations grows exponentially with the number of parameters. A simple integer XIF with two operands and a few constraints may produce thousands of combinations. A complex vector accelerator with pipeline interactions, multiple data types, and physical constraints may produce billions — far beyond practical evaluation time.

ExaVerif does not solve the combinatorial explosion problem. No tool can. What it provides is a structured approach to constraint composition that makes the scope of verification explicit. Rather than relying on random sampling and hoping coverage is sufficient, ExaVerif shows exactly which combinations were evaluated and which were deferred.

For small to medium‑sized modules — single‑cycle integer XIFs, basic cryptographic accelerators, simple state machines — exhaustive coverage is achievable. For larger designs, ExaVerif serves as a complement to existing tools, systematically covering the constraint space that random approaches might miss. The scope is narrow, and that is by design.

Competitive Landscape

Category Tool / Vendor Approach Limitation
Random simulation RISCV‑DV (Google) Constrained-random instruction generation Statistical coverage; misses deterministic edge cases
Random simulation Breker SystemVIP AI-assisted test synthesis Random seed-based; commercial license required
Formal verification OneSpin (Siemens EDA) Mathematical property proving Complex setup; verifies specific properties only
Formal verification Axiomise (formalISA) Formal property verification Requires deep formal expertise to operate
Simulation DV ImperasDV (Synopsys) Simulation-based with RVVI standard Requires commercial simulator; manual test writing
Compliance RISC‑V ACT ISA compliance test suite Limited to architectural conformance; no custom extension coverage
Cloud platform Vyoma UpTickPro Cloud-based integrated verification Verification still random/manual at core
AI debugging Vtool Cogita‑PRO AI-assisted debug Post-silicon debug; does not prevent verification gaps

What no existing tool does: exhaustive constraint composition from a single YAML description, evaluated deterministically.

Collaboration

ExaVerif welcomes collaboration with RISC‑V verification groups — including OpenHW, PULP, and individual core developers — to validate the approach against real‑world custom instruction extensions. All verification results are deposited in the shared knowledge store.

Public Assets

Asset Status
CLI (ev) Open-source (Apache 2.0)
Exhaustive engine Validated on CVA6 XIF (33.5M combos, 32s)
Spike simulation 196,608 / 196,608 pass
Shared knowledge store In development

Market Context

Figure 3: RISC-V Technology Market Size Forecast (2025–2031)
Figure 4: 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. ExaVerif’s opportunity lies in complementing existing tools for use cases where exhaustive coverage adds demonstrable value.

What Makes This Possible on RISC‑V

RISC‑V’s open ISA and fully open-source simulator infrastructure (Spike, QEMU) enable independent third-party verification that proprietary ISAs cannot support. ExaVerif leverages this openness to provide certification-grade exhaustive verification without vendor lock-in.

Roadmap

Phase 0: Foundation

Goal: Validate that the problem ExaVerif solves is real, and that the solution is technically credible.

  • Complete RISC‑V Spike integration and publish benchmarks against a public CORE‑V module
  • Interview 10 RISC‑V design teams to confirm demand for exhaustive constraint coverage
  • Submit a collaboration proposal to the OpenHW Verification Task Group
  • Output: Published benchmarks, a list of confirmed pain points, and at least one ecosystem partner engaged.

Phase 1: Working CLI + Reference Implementation

Goal: Release a functional open-source CLI with a publicly verifiable reference implementation.

  • Release ev check as open source (Apache 2.0)
  • Publish benchmarks against at least two public RISC‑V cores
  • Complete integration of the shared knowledge store for result persistence
  • Output: A single binary that performs exhaustive verification with published, reproducible benchmarks.

Phase 2: Ecosystem Validation

Goal: Determine whether the tool solves a problem that teams will pay for.

  • Secure at least two independent ecosystem partners actively using ExaVerif in their workflow
  • If validation is positive, develop paid tiers (advanced interpretation, custom templates, CI/CD integration)
  • Propose ExaVerif as a standard verification module within OpenHW’s CORE‑V‑VERIF framework
  • Output: Confirmed product-market fit or a decision to pivot.

Connection to the Substrate

ExaVerif is a neXus instance — a self-contained agentic neXus for the silicon verification domain. It does not merely “consume” neXus; it implements neXus internally. Its Spec Space exploration follows the same FIH cycle that governs every neXus entity: domain expansion is an Intent, each evaluated combination a Fact, each constraint a Hint. The Fact graph it builds over thousands of runs is its own independent, accumulated knowledge base — not a log, but a permanent, queryable, auditable body of verified knowledge.

At the same time, ExaVerif’s Facts are consumed by other neXus instances. A gap in coverage detected here becomes an Intent for OpenROAD or Yosys on the same blackboard. A verified constraint combination becomes a Hint that guides hardware synthesis elsewhere. This is not data exchange between tools; it is a single FIH graph to which every instance contributes and from which every instance reads.

This dual nature — self-contained neXus internally, co-equal peer on a larger neXus externally — is the paradigm shift the industry has not yet recognized. Existing verification tools produce PASS/FAIL logs that are discarded at the end of a run. The result has no life beyond the terminal. ExaVerif, as a neXus instance, produces Facts that are immutable, content-addressed, and permanently embedded in a graph that spans every domain of the project. A verification result is not a log entry; it is a permanent contribution to a shared body of knowledge that compounds across runs, across tools, and across time.

Figure 5: ExaVerif is the verification engine; future services would be layered on top of the shared substrate.

© 2026 SSCCS Foundation — Open-source computing systems initiative building a computing model, software compiler infrastructure, and open hardware architecture.