CVA6 CV-X-IF Exhaustive Verification Report

Deterministic encoding validation with ExaVerif (ev)

Author

Affiliation

SSCCS Foundation

SSCCS Foundation

Abstract

ExaVerif performed an exhaustive verification of the RISC-V CVA6 core’s offloadable custom instruction encodings for the CV-X-IF coprocessor interface. All 33,554,432 possible operand combinations were evaluated deterministically in 32 seconds on a single Apple M1 Max core, yielding 196,608 valid encodings. Spike cross-validation confirmed 100% correctness. This report compares the exhaustive approach to random-based verification (riscv-dv) and identifies coverage gaps on both sides.

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 32 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 32 seconds on a single laptop core.

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 196,608 valid encodings into a single ELF binary and runs it under Spike + pk. All 196,608 pass.

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

Comparison with Random Verification (riscv-dv)

Figure 3: 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.