Tandem Verification

Concept

Tandem Verification is a RISC-V testing approach in which the same generated instruction sequences are executed on a reference model and an implementation under test, and their execution traces are compared to detect divergence rather than prove full equivalence.

First seen 5/27/2026

Last seen 6/2/2026

Evidence 5 chunks

Wiki v2

WIKI

Overview

Tandem Verification is a trace-comparison approach used in the TestRIG framework for RISC-V implementations. TestRIG generates random instruction sequences, executes the same sequences on a model and an implementation under test, and compares their execution traces. The cited paper describes this as a pragmatic compromise for checking equivalence at the processor level: it does not prove equivalence, but it can demonstrate divergence and can be used throughout development. [C1]

Role in TestRIG

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

RELATIONSHIPS

4 connections

TestRIG ← implements 100% 3e

TestRIG implements tandem verification by comparing execution traces of model and implementation.

Direct Instruction Injection ← implements 90% 2e

Direct Instruction Injection enables tandem verification by providing interactive instruction injection to both model and implementation.

Tandem Execution ← implements 95% 2e

Tandem execution implements tandem verification by running the same sequences on model and implementation.

TestRIG ← uses 100% 1e

TestRIG uses tandem verification to compare RISC-V implementations against a formal model.

LINKED ENTITIES

4 links

Direct Instruction Injection IMPLEMENTS Extracted graph relationship

Tandem Execution IMPLEMENTS Extracted graph relationship

Direct Instruction Injection USES The evidence states that TestRIG uses Direct Instruction Injection for test injection, where the next instruction is provided by the test harness rather than fetched according to the program counter.

Tandem Execution USES The evidence describes executing the same generated instruction sequences on a model and implementation and comparing execution traces as 'tandem execution', which is the trace-comparison mechanism used for tandem verification.

CITATIONS

6 sources

6 citations — click to expand

[1] C1: TestRIG checks equivalence pragmatically by generating random instruction sequences, executing the same sequences on a model and implementation under test, and comparing traces; this tandem execution does not prove equivalence but can demonstrate divergence and is usable during development. Randomized Testing of RISC-V CPUs using Direct Instruction Injection

[2] C2: TestRIG uses RVFI to observe state changes after each instruction and Direct Instruction Injection to supply the next instruction from the test harness rather than from program memory according to the CPU program counter. Randomized Testing of RISC-V CPUs using Direct Instruction Injection

[3] C3: The cited work compares executable formal models, software ISA simulators, and simulated hardware designs rather than completed fabricated chips. Randomized Testing of RISC-V CPUs using Direct Instruction Injection

[4] C4: After QCVEngine finds a counterexample, QuickCheck shrinking and added smart-shrinking functions can remove or transform instructions to simplify the failing sequence. Randomized Testing of RISC-V CPUs using Direct Instruction Injection

[5] C5: Non-shrinkable sequences can preserve initialization needed to cover divergences in initial state and avoid trivial counterexamples. Randomized Testing of RISC-V CPUs using Direct Instruction Injection

[6] C6: Sequences can include assertions, and assertion failures can be found without a divergence, meaning such sequences do not require tandem verification to discover a failure. Randomized Testing of RISC-V CPUs using Direct Instruction Injection