Tandem Verification
ConceptTandem 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 7/19/2026
Evidence 6 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
NEIGHBORHOOD
2 nodes · 2 edgesgraph · Tandem Verification · depth=1
RELATIONSHIPS
4 connectionsTestRIG implements tandem verification for RISC-V implementations.
Direct Instruction Injection enables tandem verification by providing interactive instruction injection to both model and implementation.
Tandem execution implements tandem verification by running the same sequences on model and implementation.
TestRIG uses tandem verification to compare RISC-V implementations against a formal model.
LINKED ENTITIES
4 linksDirect 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 sources6 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