ExaVerif

Exhaustive Verification for RISC-V Custom Instructions

Author

Affiliation

SSCCS Initiative

Code

References

Reports

Other Formats

The Project

ExaVerif is an open-core (Apache 2.0) CLI engine for exhaustive verification of RISC-V custom instruction extensions. A single command consumes a YAML specification of a custom instruction extension, enumerates every valid combination of its fields, and evaluates each one deterministically. The specification declares every instruction field, its range, alignment, and constraints. The CLI provides three subcommands: verify for constraint evaluation, simulate for instruction execution, and synth for RTL generation and synthesis. Each result is recorded as a structured Fact, consumable by the neXus pipeline and by autonomous agents. No result is discarded; every run raises the baseline, so verification output accumulates across projects, teams, and design phases instead of resetting with each tapeout decision.

The engine verifies encoding spaces, and its only knowledge of a target is the spec it is given: no constraint type or projector carries a target’s name or constant. The cores and designs named in this documentation, CVA6 (OpenHW Group), Ibex (lowRISC), and the Tagma decoder (syntagma), are samples that exercise it. Each is described from that project’s own source, and the CVA6 encoding space is re-derived from the hardware decoder mask table at a pinned revision on every test run, so a transcription error fails rather than persists. Expansion to a broad range of additional industry silicon specifications is planned.

The Spec Space

The unit of verification is the Spec Space, a tripartite model:

Axes: field domains, each an instruction field with its admissible values.
Constraints: admissible subspaces over the axes, including oneof, range, bitmask, cross, eq, and neq.
Projector: a mapping from each point of the space to a result value.

The model is itself a complete decoder specification: axes define the inputs, constraints define the legal encodings, and the projector defines the result mapping. The same YAML compiles to synthesizable SystemVerilog through synth, so exhaustive verification doubles as design generation.

The engine compiles constraints into the enumeration itself. The iterator visits the valid space directly instead of the full cross product, so a single complete spec space verifies in milliseconds, hundreds of times faster than the standard pipeline. Because a single space is that cheap, N spec spaces run in parallel, each an observation perspective with its own constraint set, projection target, and interpretation layer. Their cross-insights compose into a multi-dimensional design map that no single pass can produce:

ev verify --target spec_space_N.xif.yaml

Identical runs produce identical records, so results stay comparable across runs and become a queryable design record that agents and design teams consult without re-executing verification. This structural enumeration is the source of the speedups measured in the benchmarks below, and it is independent of the target: any deterministic system that maps onto axes, constraints, and a projector benefits from the same pipeline.

Why the Gain Is Algorithmic

The speedup is an O(N) vs O(V) structural gain, not a language effect.

Standard evaluate_all checks every combination of the full space N; struct_enum visits the valid space V directly, constraints encoded into the enumeration.
Both pipelines are Rust, the same release build, measured by the same harness: the ratio is the enumeration strategy alone, and it survives a port to any language.
riscv-dv (UVM/simulator) and formal tools (SAT/BMC) do not enumerate at all; comparing against them is comparing apples to oranges.
Interpreted verification software (e.g., Python-based) dominates the industry landscape. The baseline here is a release-build Rust standard implementation, which in the combined assessment of memory safety-efficiency and performance already holds an overwhelming lead over C/C++; the structural gain therefore stands against an already high-performance baseline.

Benchmarks

Figure 1: Verification time: standard evaluate vs structural pipeline. With the structural pipeline integrated into the CLI (issue #42), the CVA6 33M space verifies end-to-end in about 0.2 s; the core pipeline (evaluate_structural) is 36.3 ms, ~360x faster than the naive 13.1 s.

Scaling: O(N) vs O(V)

Figure 2: Scaling across fixtures: evaluate runs in O(N), struct_enum in O(V). The gap widens as valid density drops; CVA6 full (0.6% density) shows ~700x.

Speedup follows approximately k / D (D = valid density): sparse spaces gain the most (CVA6 full 0.6% density, ~700x; Ibex 17.6%, 32x; dense spaces 1-2x).

Fixture Speedups

Fixture	Raw	Valid	evaluate	structural	Speedup
Small	27	27	4.87 µs	2.86 µs	1.7x
Medium	32,768	20,480	5.99 ms	3.02 ms	2.0x
Tagma	65,536	11,172	9.74 ms	5.94 ms	N/A (reference)
Ibex R-type	524,288	92,160	291 ms	9.10 ms	32x
CVA6 R4	16,384	2,560	3.14 ms	250 µs	13x
CVA6 full	33,554,432	196,608	13.1 s	18.8 ms	~700x
CVA6 full (evaluate_structural)	33,554,432	196,608	13.1 s	36.3 ms	361x

Status

CVA6 CV-X-IF (OpenHW): 33.5M combinations, 196,608 valid, 13.1 s vs 18.8 ms (~700x); the ev verify CLI completes the same space end-to-end in about 0.2 s (core pipeline 36.3 ms). Space derived from the hardware decoder mask table at a pinned revision and re-derived from it by a gate in the test suite; the DV class generates encodings the decoder rejects, a documented divergence. Master report: CVA6 CV-X-IF Report (Standard Reference).
Ibex RV32IMCB (lowRISC): 524,288 combinations, 92,160 valid, 291 ms vs 9.10 ms (32x); evaluate_structural core 16.2 ms. Report: Ibex RV32IMCB Report.

Limits

Exhaustive coverage grows exponentially with parameters; the speedup depends on valid-space density, not raw size.
Counts are field-value combinations and equal distinct instruction words (no enable_mask collapsing in the CVA6 fixtures).

Ev is a project of the SSCCS Initiative. Inquiries: ev@ssccs.org.