CVA6 CV-X-IF Exhaustive Verification Report

Deterministic encoding validation with ExaVerif (ev)

Author

Affiliation

SSCCS Foundation

SSCCS Foundation

Abstract

ExaVerif performed exhaustive verification of the RISC-V CVA6 core’s offloadable custom instruction encodings for the CV-X-IF coprocessor interface. The standard pipeline evaluates all 33,554,432 operand combinations in 29.7 seconds on a single ARMv8.4-A Firestorm system, yielding 229,376 valid encodings. The Tagma-based structural enumeration evaluates the same space in 31.3 milliseconds (structural_verify with all constraint checks) – a ~950x improvement – by generating only structurally valid combinations. At the CVA6 R4 fixture (2M combinations), struct_enum achieves 764x speedup (1.23 s vs 1.61 ms). Spike cross-validation confirms 100% correctness.

Code

Github

Benchmarks

bench.rs

Fixture

CVA6 XIF spec

References

neXus

OpenHW

Other Formats

LLMs

Verification Target

The CVA6 core (Ariane, OpenHW Group) offloads custom instructions to a coprocessor through the CV-X-IF interface whenever the core decoder encounters an illegal instruction. Four RISC-V custom opcode spaces (custom-0 through custom-3) are always illegal and therefore always offloadable. This verification covers the custom-3 opcode (0x7B) encoding space as defined by the CVA6 verification suite.

Six instructions are defined within this space, decoded by the coprocessor through a combination of the funct3 and funct7 fields:

funct3	funct7	Instruction	Operand registers
0	2, 6, 8, 32	ADD variants	rs1, rs2 [, rs3]
1	0	CUS_ADD	rs1, rs2
2	96	CUS_EXC	rs1
3..7	any	illegal	—

Exhaustive Verification Results

Figure 1: CVA6 XIF encoding space verification: 33.5M combinations evaluated in 29.7 seconds. Valid encodings are concentrated in three narrow funct3 bands; the remaining 99.4% are correctly rejected as illegal.

Speed and Scale

Figure 2: Verification time comparison across three approaches for the CVA6 XIF encoding space. ExaVerif completes in 29.7 seconds on a single laptop core.

Structural Enumeration Performance

Figure 3: Verification time: standard evaluate (1.23s for R4, 29.7s for full 33M) vs struct_enum (1.61ms for R4, 31.3ms for full). At CVA6 2M scale, struct_enum achieves 764x speedup.

Scaling: O(N) vs O(V)

Figure 4: Scaling behavior: evaluate runs in O(N) where N is the full encoding space; struct_enum runs in O(V) where V is the structurally valid subset. CVA6 R4 (0.6% density) shows 764x speedup; denser spaces see lower but still significant gains.

Benchmark Results (ARMv8.4-A Firestorm)

Figure 5: Complete benchmark data including CVA6 fixtures. struct_enum achieves 79x–950x speedup over the standard pipeline across all real-world RISC-V verification targets.

How It Works

A single YAML file describes the encoding space and its constraints. The entire space is enumerated exhaustively and evaluated deterministically — every point is classified as valid or invalid based on the specification.

ev verify --target cva6_xif_ref.xif.yaml

Every valid encoding can also be verified through actual RISC-V simulation. ExaVerif packs all 229,376 valid encodings into a single ELF binary and runs it under Spike + pk. All 229,376 pass.

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

Structural vs Standard: the mechanism

Aspect	Standard (evaluate)	Structural (struct_enum)
Combinations generated	All 33,554,432	Valid only 229,376
Constraint evaluation	10 checks × 33.5M	0 (structurally encoded)
Invalid detection	check.allows() → false	Vacant slot → 1.65 ns
Memory	4 GB peak (Vec)	0 (lazy iterator)
Time (CVA6 R4)	1.23 s	1.61 ms
Time (CVA6 full)	29.7 s	31.3 ms

Comparison with synTagma Benchmarks

The struct_enum speedup mirrors synTagma’s core thesis: structural addressing eliminates hash-based lookup overhead.

synTagma primitive	ev application	Measured	Advantage
Nonexistent prefix lookup	Invalid encoding detection	1.65 ns	14.0Mx vs HashMap
CoordPath indexing	Combination addressing	5.2 ns	O(depth) = O(5)
CoordSpace sparse get	Valid encoding iteration	1.61 ms (2M space)	764x vs evaluate
Axis projection	funct7/funct3 filtering	46.3 ms (524K space)	79x vs evaluate

Comparison with Random Verification (riscv-dv)

Figure 6: Unique encoding coverage: exhaustive enumeration covers 33.5x more encodings than random sampling, with deterministic certainty.

Limitations

What ExaVerif does not yet model

• NOP instruction: CUS_NOP disables all register operands. A mechanism for conditional field activation is needed.
• func2 field: CUS_ADD_RS3 uses a dedicated func2 bit field, currently simplified into the funct7 domain.
• Weighted register distribution: CUS_EXC biases certain register values. ExaVerif treats all register values uniformly.
• Pipeline hazards: Write-after-read hazards (rs1==rd) are not modelled at the encoding level.