# CVA6 CV-X-IF Exhaustive Verification Report

Deterministic encoding validation with ExaVerif (ev)

Author

Affiliation

SSCCS Foundation [](mailto:contact@ssccs.org)

[SSCCS Foundation](https://ssccs.org)

Published

June 4, 2026

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](https://docs.ssccs.org/projects/ev/cva6.llms.md)

## 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

![](cva6_files/figure-html/fig-verification-scale-output-1.svg)

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

![](cva6_files/figure-html/fig-speed-comparison-output-1.svg)

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.

``` bash
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.

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

## Comparison with Random Verification (riscv-dv)

![](cva6_files/figure-html/fig-coverage-comparison-output-1.svg)

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.