Assertions in Instruction Sequences

Concept

Assertions in instruction sequences are explicit checks embedded in generated CPU test traces. In TestRIG/QCVEngine workflows, they can make a sequence fail without requiring a tandem-verification divergence, and have been used to test implementation-defined behavior and to express deterministic microarchitectural checks such as cache-counter expectations.

First seen 5/27/2026

Last seen 5/27/2026

Evidence 2 chunks

Wiki v1

WIKI

Overview

Assertions in instruction sequences are checks embedded directly in a generated instruction trace. The TestRIG paper describes sequences that can include assertions, such as checking that the value written by the previous instruction was non-zero. These assertions allow a generated sequence to fail even when no divergence has been observed between tandem executions or reference comparisons. The authors note that, unusually, such sequences do not require tandem verification to discover a failure, and that they have used assertions to test the limits of implementation-defined behavior.

Role in randomized CPU testing

READ FULL ARTICLE →

NEIGHBORHOOD

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

explore full graph →

RELATIONSHIPS

2 connections

QCVEngine ← uses 90% 2e

QCVEngine supports assertions in instruction sequences to detect failures without divergence.

TestRIG ← uses 90% 2e

TestRIG supports assertions in instruction sequences to detect failures without requiring tandem verification.

LINKED ENTITIES

2 links

QCVEngine USES Extracted graph relationship

TestRIG USES Extracted graph relationship

CITATIONS

5 sources

5 citations — click to expand

[1] Instruction sequences can include assertions, for example checking that the previous instruction wrote a non-zero value. Randomized Testing of RISC-V CPUs using Direct

[2] Assertions make it possible for a sequence to fail without a divergence and do not require tandem verification to discover a failure. Randomized Testing of RISC-V CPUs using Direct

[3] Assertions have been used to test the limits of implementation-defined behavior. Randomized Testing of RISC-V CPUs using Direct

[4] A TestRIG counterexample used both `.noshrink` and `.assert`, with `.noshrink` preserving counter initialization so that the final L1 cache-miss-counter assertion was deterministic. Randomized Testing of RISC-V CPUs using Direct

[5] In the illustrated CHERI counterexample, illegal `cSetBoundsImmediate` attempted to enlarge capability bounds, threw an exception, but the would-be capability was forwarded during pipeline flush and caused a cache fill that could lead to side-channel attacks. Randomized Testing of RISC-V CPUs using Direct