Overview

Tandem Execution is the execution-and-comparison pattern used during tandem verification: executable formal models, software ISA simulators, and simulated hardware designs are compared rather than testing completed fabricated chips. In the cited RISC-V setting, this requires instrumenting the CPU design with a Direct Instruction Injection interface used by the test harness during tandem verification. [tandem-scope]

Method

A verification engine drives one or more RISC-V implementations by injecting instruction sequences and consuming their execution traces. The technique detects errors by comparing traces and stopping when a divergence is found. [trace-comparison]

In TestRIG, the interactive Verification Engine, or VEngine, stimulates RISC-V implementations over RVFI-DII sockets. An RVFI-DII-compatible implementation can reset, consume instruction sequences, and report execution traces through its RVFI-DII interface. [testrig-architecture]

Inputs and execution targets

Instruction sequences used by the verification engine may be loaded from disk, generated randomly, or produced through interactive architecture-driven state-space exploration. [sequence-sources]

The compared execution targets may include an internal RISC-V model or two independent implementations whose RVFI traces are compared. The evidence specifically describes Direct Instruction Injection support being added to the Sail RISC-V formal model, Spike, and QEMU, and also describes instrumentation of multiple RISC-V processor implementations with RVFI-DII. [targets]

Relationship to TestRIG

TestRIG implements this technique by using a VEngine to inject instruction sequences over RVFI-DII sockets and compare execution traces until it finds a divergence. [testrig-architecture]