Overview

RVFI-DII (pronounced "rividy") is the combined verification interface used by the TestRIG framework. It joins the RISC-V Formal Interface (RVFI), a tracing protocol for RISC-V processors that specifies the results of running instructions, with Direct Instruction Injection (DII), in which the next instruction is supplied by the test harness rather than fetched from program memory. TestRIG describes itself as "a framework for RISC-V processor verification using the RVFI-DII interface," and the full wire format is documented in the project repository's RVFI-DII specification.

Components and data flow

TestRIG distinguishes two kinds of components that communicate over RVFI-DII:

• Vengines (verification engines) generate one or more DII streams of instruction traces and consume one or more RVFI streams of execution traces.
• Implementations (including models, simulators, and SoCs) consume a DII instruction trace and generate an RVFI execution trace.

A vengine typically includes instruction trace (itrace) generators targeting various classes of behaviour. It feeds the itraces into both a model and an implementation through two TCP sockets in the RVFI-DII format. The model and implementation return an RVFI-DII execution trace (etrace) that details the state observation and state change of each instruction. The vengine compares these two traces and identifies any divergence between the model and the implementation. Any failure is reported with a means of conveniently replaying the failing itrace for debugging, and a capable vengine will also attempt to reduce the failing trace to a minimal example that diverges.

The RVFI-DII communication uses a single socket per implementation: the itrace is consumed and the etrace is delivered over the same socket.

Execution and trace model

The evidence distinguishes normal execution from DII execution. In normal execution, the next instruction is fetched from program memory at an address determined by the program counter. Under DII, the implementation consumes instructions exclusively from the RVFI-DII instruction port, bypassing any actual instruction memory and ignoring the architectural program counter. The implementation then delivers a trace report at the end of execution detailing its behaviour in response to that instruction in the RVFI-DII format.

Role in TestRIG

TestRIG checks equivalence between a RISC-V model and an implementation under test by generating random instruction sequences, executing the same sequences on both sides, and comparing execution traces. Within that workflow, RVFI provides the observation path and DII provides the injection path.

Use cases and rationale

The TestRIG documentation positions RVFI-DII as a way to eliminate the "test gap" between specification and implementation. By using an executable model as the specification, TestRIG allows automated verification of any specified property without passing through human interpretation and hand-writing tests, and new instructions in an existing class can automatically be included in new traces and run in many more variations than hand-written tests would allow. RVFI-DII also verifies the pipeline as well as specification compliance: under random sequence generation, every register value read in the pipeline can be observed, whereas a fixed test suite would only report a prescribed test result. Because DII bypasses fetch through the PC, a sequence of instructions can easily be shortened by simply eliminating instructions from the trace to see if divergence still occurs, leading to automatically reduced counterexamples on the order of a handful of instructions.

Single-implementation mode

Aligning an implementation and a model on every possible instruction input is hard (for example, CSR legalisation, store-conditional failures, and misaligned accesses). To allow more liberal testing without having to reason about control flow, TestRIG supports a "single implementation" mode in which the implementation is run on its own and more liberal properties are asserted over the RVFI trace. An example property is that the instruction count in equals the instruction count out, ensuring that the processor did not lock up. DII is required to enable this style of testing, and the technique has been used to find and diagnose cases such as a processor mis-decoding and locking up on certain illegal instructions, a subtle and rare compressed-branch mispredict infinite loop, and a reachable fatal assert in a version of the Sail model.

Relationship to related concepts

• RVFI: The tracing protocol half of RVFI-DII; specifies the results of running each instruction and is consumed from implementations as part of an etrace.
• DII Stream: The instruction injection half of RVFI-DII; produced by vengines and consumed by implementations as the itrace.
• RVFI Stream: The execution trace half; produced by implementations and consumed by vengines for comparison.
• TestRIG: The framework built around RVFI-DII; the repository and paper document the interface and the open-source comparison tooling that surrounds it.
• Sail RISC-V Model: One of the standard executable ISA specifications usable as a TestRIG reference model, compiled and compared against implementations via RVFI-DII.