Skip to content
STIMSMITH

Assertions in Instruction Sequences

Concept WIKI v1 · 5/27/2026

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.

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

In the TestRIG/QCVEngine context, assertions complement randomized instruction generation and shrinking. A normal randomized test may expose a bug through divergence, after which shrinking reduces the counterexample. Assertions add another failure mechanism: the test can encode a property that must hold at a particular point in the instruction sequence. If the property is violated, the sequence fails even without a comparator-observed architectural mismatch.

Example: cache-counter assertion in a CHERI-RISC-V counterexample

One illustrated counterexample combines .noshrink and .assert. The sequence initializes counters, performs an illegal cSetBoundsImmediate that attempts to enlarge a CHERI capability bound, executes a load through the resulting illegal capability, delays for counter propagation, reads the L1 cache-miss counter, and then asserts:

.assert rd_wdata == 0x0 ""

The paper explains that .noshrink is used to initialize counter state so that the final assertion on the L1 cache-miss counter is deterministic. The same example is used to demonstrate a vulnerability: although CHERI only allows bounds to be reduced and the illegal cSetBoundsImmediate throws an exception, the capability that would have been produced is forwarded during a pipeline flush and causes a cache fill that could lead to side-channel attacks.

Relationship to non-shrinkable sequence regions

Assertions may be used alongside non-shrinkable regions. The cited example uses .noshrink to preserve initialization needed for determinism, while .assert records the expected final condition. This pairing is useful when shrinking would otherwise remove setup code required to make an assertion meaningful or repeatable.

Practical significance

Assertions make instruction sequences more expressive than pure divergence-based tests. They allow generated tests to encode properties over observed instruction results or machine counters, supporting checks for implementation-defined behavior and microarchitectural effects that may not appear as ordinary architectural divergences.

LINKED ENTITIES

2 links
QCVEngine USES
TestRIG USES

CITATIONS

5 sources
5 citations
[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