Skip to content
STIMSMITH

Verification Engine

Concept WIKI v1 · 5/30/2026

A verification engine is the checking component in a verification workflow. In the TestRIG RISC-V CPU testing context, the concrete verification engine is QCVEngine, which uses Haskell QuickCheck with Direct Instruction Injection and RVFI traces to generate, compare, and shrink randomized instruction-sequence tests.

Overview

A verification engine is the component that drives and evaluates tests or proof obligations against a correctness criterion. In the TestRIG RISC-V CPU-testing workflow, the verification engine is represented by QCVEngine, described as the “TestRIG Verification Engine.” QCVEngine leverages Haskell’s QuickCheck library to generate instruction sequences, compare execution traces, and shrink failing examples.

Role in TestRIG

TestRIG uses Direct Instruction Injection (DII) and RVFI traces to compare behavior across implementations. DII directly specifies the instruction sequence expected in the output trace and does not associate instructions with memory addresses. This decouples the instruction stream from control flow, which simplifies sequence generation and shrinking because the program counter does not affect the instruction stream.

QCVEngine takes advantage of this structure by using unmodified QuickCheck utilities. Its core test function receives a list of instructions, sends them over two DII sockets, collects RVFI traces from those sockets, asserts that the traces match, and returns a pass/fail result to QuickCheck.

Test generation and shrinking

QCVEngine provides generators for arbitrary instruction sequences. It also uses convenience functions that resemble the RISC-V ISA manual syntax and tailored generators for instruction fields, including generator choices intended to promote register reuse. QuickCheck discovers and uses these generators through Haskell’s type system.

The engine also supports more targeted generation strategies. The cited TestRIG work describes targeted generators for simple instruction-set subsets and generators based on templates of varying complexity, including templates intended to reach deeper states such as virtual-memory mappings and cache conflicts.

Because QuickCheck searches for failing inputs and shrinks them, QCVEngine can provide reduced counterexamples. The TestRIG paper reports that this tight cycle of reduced counterexamples helped add functionality to Ibex within a month.

Trace replay and equivalence checking

The TestRIG authors report using QCVEngine-related trace features to replay recorded test-suite examples, including examples from riscv-tests and RISCV-DV, while adding full trace-equivalence checking with shrinking. They also report capturing traces of an operating system booting on a model implementation, then using those traces to aid bring-up on implementations, with instruction shrinking helping to highlight problems.

Current limitations and future direction

The TestRIG paper characterizes QCVEngine as the initial TestRIG verification engine and says its generators were still rudimentary at the time of writing. Although its Haskell infrastructure supports rich and complex generators, the authors identify virtual-memory, cache-testing, and floating-point generators as areas that could be enriched with more intelligent directed-random templates for reaching deeper states.

The same paper also identifies memory-model and concurrency testing as future work. It proposes that RVFI-DII instruction streams with specified timestamps, injected into multiple shared-memory cores, could precisely stimulate concurrency behavior. That use case would require a more advanced verification engine that checks RVFI traces not only for equivalence but also against higher-level memory-model semantics.

LINKED ENTITIES

2 links
QCVEngine IMPLEMENTS
TestRIG DEPENDS_ON

CITATIONS

8 sources
8 citations
[1] QCVEngine is described as the TestRIG Verification Engine and uses Haskell QuickCheck. Randomized Testing of RISC-V CPUs using Direct
[2] DII decouples the instruction stream from control flow, enabling simplified generation and shrinking. Randomized Testing of RISC-V CPUs using Direct
[3] QCVEngine's QuickCheck function sends instruction lists over two DII sockets, collects RVFI traces, checks that they match, and returns a pass/fail result. Randomized Testing of RISC-V CPUs using Direct
[4] QCVEngine provides arbitrary and targeted instruction generators, including template-based generators for deeper states such as virtual-memory mappings and cache conflicts. Randomized Testing of RISC-V CPUs using Direct
[5] QCVEngine-supported replay can add full trace-equivalence checking with shrinking to recorded test-suite examples such as riscv-tests and RISCV-DV. Randomized Testing of RISC-V CPUs using Direct
[6] The TestRIG authors describe QCVEngine's initial generators as rudimentary and identify richer virtual-memory, cache, and floating-point generators as future work. Randomized Testing of RISC-V CPUs using Direct
[7] Future TestRIG memory-concurrency testing would require a more advanced verification engine that checks RVFI traces against higher-level memory-model semantics as well as equivalence. Randomized Testing of RISC-V CPUs using Direct
[8] The TestRIG repository collates TestRIG-compatible implementations and verification engines. Randomized Testing of RISC-V CPUs using Direct