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.

Comparison

Metric	Random Simulation	Formal Verification	Ev
Combinations evaluated	~10⁶ (sampled)	~10³ (properties)	33.5 × 10⁶ (exhaustive)
Coverage guarantee	Statistical	Formal (per property)	Exhaustive
Setup	UVM + agent	Formal properties	Single spec file
Cross-validated	—	—	Spike simulation

Status and Limits

Validated against a production RISC-V core interface (CVA6 CV-X-IF, 33.5 million combinations, 32 seconds), cross-verified through Spike simulation.

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.