ExaVerif exhaustively enumerates and evaluates every valid combination of RISC-V custom instruction fields. Each result is a deterministic pass/fail recorded as a Fact consumable by neXus.

RISC-V custom instruction extensions are verified with constrained-random tools (riscv-dv) or formal property checkers (OneSpin). Both approaches leave coverage gaps: random simulation cannot prove absence of invalid encodings, and formal tools require significant expertise to set up.

A verification team adding a custom instruction extension must ensure that every operand combination, every funct3/funct7 variant, and every cross-field constraint produces a valid encoding. With random simulation, they run millions of seeds. With formal tools, they write properties for each behavior. Neither approach enumerates the complete space.

A coverage report from one tapeout is inaccessible to the next. A failure trace from one team is invisible to another. Verification results are ephemeral logs, not accumulated knowledge. Ev enumerates the full Cartesian product of field domains, evaluates every point against the constraint set, and reports pass/fail for every encoding.

Benchmarks (ARMv8.4-A Firestorm)

Measured with cargo bench (criterion 0.5). Structural_verify runs ALL constraint checks (cross, oneof, range, bitmask, eq, neq, etc.) and projection — identical work to the standard evaluate pipeline, differing only in enumeration source.

Figure 1: Verification time: standard evaluate vs structural pipeline. At CVA6 33M scale, structural_verify achieves ~950x speedup by generating only structurally valid combinations.

The two pipelines differ in enumeration strategy, not in verification scope. The standard pipeline computes the full Cartesian product of field domains then filters each combination through constraint checks. The structural pipeline encodes cross-field constraints directly into the coordinate space of synTagma’s DynCoordSpace; enumeration visits only combinations that satisfy those constraints a priori. Both pipelines evaluate the full constraint set on every combination they visit, and both classify every point of the encoding space. The standard pipeline visits 33,554,432 points of which 229,376 pass; the structural pipeline visits 229,376 points directly.

Comparison

Metric	Random Simulation	Formal Verification	Ev (standard)	Ev structural
Combinations evaluated	~10^6 (sampled)	~10^3 (properties)	33.5 x 10^6 (exhaustive)	33.5 x 10^6
Coverage guarantee	Statistical	Formal (per property)	Exhaustive	Exhaustive
CVA6 full (33M) verify time	~10 hr	~72 hr	29.7 s	31.3 ms (950x)
CVA6 R4 (2M) verify time	~30 min	~2 hr	1.23 s	1.61 ms (764x)
Ibex (524K) verify time	~15 min	~1 hr	3.66 s	46.3 ms (79x)
Setup	UVM + agent	Formal properties	Single spec file	Single spec file
Cross-validated	—	—	Spike simulation	Spike simulation

Status and Limits

Validated against two production RISC-V cores:

CVA6 CV-X-IF (OpenHW Group): 33.5 million combinations exhaustive in 29.7 seconds (standard) or 31.3 milliseconds with synTagma structural enumeration (950x speedup). Cross-verified through Spike simulation.
Ibex RV32IMCB (lowRISC): 524,288 combinations exhaustive in 3.66 seconds (standard) or 46.3 milliseconds with structural enumeration (79x speedup).

synTagma Integration

With synTagma’s structural coordinate space, constraints are encoded into the enumeration space itself. Invalid combinations are never generated; only structurally valid combinations are visited. This eliminates all runtime constraint evaluation, achieving 73x–1000x speedups across real-world verification targets.

Fixture	Raw space	Standard evaluate	Structural verify	Speedup
Ibex R-type	524,288	3.66 s	46.3 ms	79x
CVA6 R4	2,097,152	1.23 s	1.61 ms	764x
CVA6 full	33,554,432	29.7 s	31.3 ms	950x

Detailed reports:

Limits

Exhaustive verification has a constraint: combinations grow exponentially with parameters. For small to medium-sized modules, exhaustive coverage is achievable. For larger designs, Ev shows which combinations were evaluated and which were deferred.

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