Execution Trace

Concept

An execution trace is a structured, time-ordered record of state observations and state changes produced as a system executes a sequence of operations. In the RISC-V verification ecosystem — specifically TestRIG, which uses the RVFI-DII interface — an implementation generates a per-instruction RVFI execution trace (etrace) in response to an injected DII instruction trace (itrace), and a verification engine (vengine) compares the execution traces from a reference model and an implementation under test to detect divergence. Execution traces are produced by instrumented hardware designs, ISA simulators, and formal models, and are consumed by verification engines, debuggers, and program-repair systems.

First seen 5/29/2026

Last seen 8/11/2026

Evidence 12 chunks

Wiki v2

WIKI

Overview

An execution trace is a structured, time-ordered record of the state observations and state changes that occur as a system executes a sequence of operations. Execution traces are produced by instrumented hardware designs, ISA simulators, formal models, or instrumented software, and they are consumed by verification engines, debuggers, and program-repair systems in order to detect divergence between actual and expected behavior.

Execution Traces in RISC-V Processor Verification (TestRIG / RVFI-DII)

READ FULL ARTICLE →

NEIGHBORHOOD

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

explore full graph →

RELATIONSHIPS

1 connections

RVFI Stream part of → 1e

An RVFI Stream carries Execution Traces.

LINKED ENTITIES

1 links

RVFI Stream aggregation_of_execution_traces The TestRIG documentation explicitly says vengines consume 'one or more RVFI streams of execution traces', implying execution traces are the constituent elements of an RVFI stream.

CITATIONS

11 sources

11 citations — click to expand

[1] TestRIG is a framework for RISC-V processor verification using the RVFI-DII interface. GitHub - CTSRD-CHERI/TestRIG: Testing processors with Random Instruction Generation

[2] Vengines generate one or more DII streams of instruction traces, and consume one or more RVFI streams of execution traces; implementations consume a DII instruction trace and generate an RVFI execution trace. GitHub - CTSRD-CHERI/TestRIG: Testing processors with Random Instruction Generation

[3] The model and implementation return an RVFI-DII execution trace (etrace) that details the state observation and state change of each instruction. GitHub - CTSRD-CHERI/TestRIG: Testing processors with Random Instruction Generation

[4] The vengine feeds itraces into both a model and an implementation through two TCP sockets in the RVFI-DII format, compares the two traces, and a capable vengine will attempt to reduce the failing trace to a minimal example that diverges. GitHub - CTSRD-CHERI/TestRIG: Testing processors with Random Instruction Generation

[5] Implementations verified by TestRIG must support RVFI-DII itrace as the instruction source and etrace as the reporting format; instructions are consumed exclusively from the RVFI-DII instruction port, bypassing any actual instruction memory and ignoring the architectural program counter. GitHub - CTSRD-CHERI/TestRIG: Testing processors with Random Instruction Generation

[6] The RVFI-DII communication uses a single socket with the itrace consumed and the etrace delivered over the same socket. GitHub - CTSRD-CHERI/TestRIG: Testing processors with Random Instruction Generation

[7] TestRIG eliminates the test gap between specification and implementation and, with an executable model specification, allows automated verification of any specified property without passing through human interpretation and hand-writing tests. GitHub - CTSRD-CHERI/TestRIG: Testing processors with Random Instruction Generation

[8] TestRIG verifies the pipeline as well as specification compliance by verifying every register value read in the pipeline under random sequence generation, while a test suite only reports a prescribed test result. GitHub - CTSRD-CHERI/TestRIG: Testing processors with Random Instruction Generation

[9] Because TestRIG relies on direct instruction injection bypassing fetch through PC, a sequence of instructions can be shortened by eliminating instructions from the trace to find divergence, yielding automatically reduced counterexamples on the order of a handful of instructions. GitHub - CTSRD-CHERI/TestRIG: Testing processors with Random Instruction Generation

[10] The TestRIG root makefile can currently build the QuickCheck Verification Engine, Spike, and the Sail implementation; Spike and Sail are built without CHERI support by default and Sail is built as a 32-bit version. GitHub - CTSRD-CHERI/TestRIG: Testing processors with Random Instruction Generation

[11] TestRIG can be invoked to compare Sail against Toooba on 64-bit RISC-V using `utils/scripts/runTestRIG.py -a sail -b toooba -r rv64i`, and to compare Sail against Ibex on 32-bit CHERI RISC-V using `utils/scripts/runTestRIG.py -a sail -b ibex -r rv32icxcheri`. GitHub - CTSRD-CHERI/TestRIG: Testing processors with Random Instruction Generation