Test Case Shrinking

Technique

Test case shrinking is used in RISC-V CPU verification to turn generated instruction sequences into smaller counterexamples or minimal tests. In TestRIG, direct instruction injection makes shrinking sequences with branches straightforward, and shrink/no-shrink annotations can preserve deterministic setup while isolating failing behavior.

First seen 5/30/2026

Last seen 5/31/2026

Evidence 7 chunks

Wiki v1

WIKI

Overview

Test case shrinking is a verification technique for reducing generated instruction sequences into smaller counterexamples or minimal tests while preserving the behavior needed to demonstrate a bug. In the supplied RISC-V CPU verification evidence, shrinking appears in two closely related forms: TestRIG uses direct instruction injection to make shrinking instruction sequences, including sequences with branches, straightforward; Symbolic QED is described as generating minimal tests for verification, including post-silicon verification, using a formal model of the pipeline.

Use 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

7 connections

TestRIG ← uses 100% 2e

TestRIG uses test case shrinking to reduce counterexamples to minimal failing sequences.

QCVEngine ← uses 100% 2e

QCVEngine uses QuickCheck's builtin shrinking and smart shrinking functions to reduce failing test sequences.

Symbolic QED ← uses 80% 1e

Symbolic QED generates minimal tests using formal models.

C-Reduce ← uses 95% 1e

C-Reduce performs automated reduction of failing test cases for C compilers.

PyH2P ← uses 95% 1e

PyH2P applies automated test case reduction to randomly generated RISC-V instruction sequences.

Smart Shrinking ← extends 95% 1e

Smart shrinking extends test case shrinking by intelligently transforming instructions rather than just eliminating them.

otbn-rig ← mentions 1e

otbn-rig mentions potential future support for test case shrinking.

LINKED ENTITIES

6 links

TestRIG USES Extracted graph relationship

QCVEngine USES Extracted graph relationship

Symbolic QED USES Extracted graph relationship

C-Reduce USES Extracted graph relationship

PyH2P USES Extracted graph relationship

Smart Shrinking EXTENDS Extracted graph relationship

CITATIONS

6 sources

6 citations — click to expand

[1] TestRIG uses direct instruction injection, and instruction injection allows straightforward shrinking of instruction sequences with branches. Randomized Testing of RISC-V CPUs using Direct

[2] A TestRIG shrunken counterexample used .noshrink, .shrink, and .assert directives to demonstrate a CHERI cSetBoundsImmediate vulnerability. Randomized Testing of RISC-V CPUs using Direct

[3] .noshrink was used to preserve initialization needed for a deterministic final assertion on the L1 cache-miss counter. Randomized Testing of RISC-V CPUs using Direct

[4] The cSetBoundsImmediate counterexample showed an illegal bounds-enlarging operation that threw an exception, while a forwarded capability during pipeline flush caused a cache fill that could lead to side-channel attacks. Randomized Testing of RISC-V CPUs using Direct

[5] Symbolic QED generates minimal tests for verification, including post-silicon verification, using a formal pipeline model. Randomized Testing of RISC-V CPUs using Direct

[6] TestRIG has been used to find architectural bugs, microarchitectural mistakes such as forwarding or pipeline-flush problems, memory mistakes such as cache bugs or memory speculation failures, and unexpected interactions between architectural features. Randomized Testing of RISC-V CPUs using Direct