Skip to content
STIMSMITH

Verification Engine (VEngine)

Concept WIKI v1 · 5/27/2026

In TestRIG, the verification engine is represented by QCVEngine, a Haskell QuickCheck-based engine that generates, compares, and shrinks Direct Instruction Injection instruction sequences and checks returned RVFI traces for equivalence.

Overview

A Verification Engine (VEngine) in the TestRIG context is exemplified by QCVEngine, described as the TestRIG Verification Engine. QCVEngine leverages Haskell’s QuickCheck library and uses the simplicity of Direct Instruction Injection (DII) execution to generate, compare, and shrink instruction sequences. DII decouples the instruction stream from control flow, allowing QCVEngine to use unmodified QuickCheck utilities for these tasks.

Trace-equivalence workflow

QCVEngine is built around QuickCheck’s model of receiving a function with a pass/fail return value and generating inputs in search of a failure. The described TestRIG setup constructs a function that:

  1. receives a list of instructions,
  2. sends those instructions over two DII sockets,
  3. collects RVFI traces back from the sockets,
  4. asserts that the traces match, and
  5. returns the result.

This makes the engine a randomized trace-equivalence checker for implementations or models connected through DII and RVFI trace reporting.

Instruction generation

QCVEngine provides generators for arbitrary instruction sequences. It also uses convenience functions to define instructions in syntax closely resembling the RISC-V ISA manual, with tailored generators for instruction fields to promote register reuse. QuickCheck discovers and uses these generators through Haskell’s type system to construct arbitrary instruction sequences.

Beyond arbitrary generation, QCVEngine includes targeted generators for simple subsets of the instruction set and template-based generators intended to reach deeper states, including virtual-memory mappings and cache conflicts.

Shrinking and replay

The engine supports shrinking of counterexamples as part of its QuickCheck workflow. The evidence also describes use of this capability to replay recorded test-suite examples, including riscv-tests and RISCV-DV, adding full trace-equivalence checking with shrinking. The same trace-replay feature was used to capture traces of an operating system booting on a model implementation and then use those traces to aid bring-up of the same operating system on implementations, with instruction shrinking helping to highlight problems.

Limitations and future direction

The initial QCVEngine generators are described as still rudimentary. The evidence identifies virtual memory, cache testing, and floating-point operations as areas where generators could be enriched with more intelligent directed-random templates to reach deeper states.

For future TestRIG memory-concurrency testing, the evidence suggests that RVFI-DII instruction streams with specified timestamps could be injected into multiple shared-memory cores to stimulate concurrency behavior. That capability would require a more advanced verification engine that tests RVFI traces not only for equivalence, but also against higher-level memory-model semantics.

LINKED ENTITIES

1 links
TestRIG USES

CITATIONS

7 sources
7 citations
[1] QCVEngine is described as the TestRIG Verification Engine and leverages Haskell’s QuickCheck library. Randomized Testing of RISC-V CPUs using Direct
[2] Because DII decouples the instruction stream from control flow, QCVEngine can use unmodified QuickCheck utilities to generate, compare, and shrink instruction sequences. Randomized Testing of RISC-V CPUs using Direct
[3] The QCVEngine checking function sends a list of instructions over two DII sockets, collects RVFI traces, asserts that they match, and returns the result. Randomized Testing of RISC-V CPUs using Direct
[4] QCVEngine provides arbitrary instruction-sequence generators, targeted instruction-subset generators, and template-based generators for deeper states such as virtual-memory mappings and cache conflicts. Randomized Testing of RISC-V CPUs using Direct
[5] QCVEngine has been used to replay recorded test-suite examples, including riscv-tests and RISCV-DV, with full trace-equivalence checking and shrinking. Randomized Testing of RISC-V CPUs using Direct
[6] The initial QCVEngine generators are described as rudimentary, with virtual memory, cache testing, and floating-point operations identified as areas for richer directed-random templates. 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 not only for equivalence but also against higher-level memory-model semantics. Randomized Testing of RISC-V CPUs using Direct