Counterexample-Driven Development

Concept

Counterexample-driven development is a processor-design workflow described in the TestRIG paper in which model-based testing produces reduced counterexamples that guide debugging and implementation. The paper presents it as an advancement over conventional test-driven development for processor design because TestRIG can provide reduced stimulus for basic features before ordinary architectural unit tests are practical, and can continue supporting development through advanced interactions.

First seen 5/27/2026

Last seen 6/3/2026

Evidence 2 chunks

Wiki v2

WIKI

Overview

Counterexample-driven development is a processor-development workflow in which model-based testing produces reduced counterexamples that guide implementation and debugging. In the TestRIG paper, the authors state that TestRIG’s model-based testing leads to this workflow and describe it as an advancement over conventional test-driven development in processor design. [C1]

Relationship to TestRIG

READ FULL ARTICLE →

NEIGHBORHOOD

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

explore full graph →

RELATIONSHIPS

5 connections

TestRIG ← implements 100% 5e

TestRIG's model-based testing leads to counterexample-driven development.

TestRIG ← uses 95% 1e

TestRIG's model-based testing leads to counterexample-driven development.

Randomized Testing of RISC-V CPUs using Direct Instruction Injection ← evaluates 90% 1e

The paper discusses counterexample-driven development as an advancement over test-driven development.

QCVEngine ← implements 90% 1e

QCVEngine supports counterexample-driven development by continuously providing reduced counterexamples during development.

Test-Driven Development extends → 95% 1e

Counterexample-driven development is an advancement over test-driven development for processor design.

LINKED ENTITIES

2 links

TestRIG USES Extracted graph relationship

Randomized Testing of RISC-V CPUs using Direct Instruction Injection EVALUATES Extracted graph relationship

CITATIONS

5 sources

5 citations — click to expand

[1] TestRIG’s model-based testing leads to counterexample-driven development, which the paper presents as an advancement over test-driven development for processor design; TestRIG can provide reduced stimulus for basic features and carry development through advanced interactions. Randomized Testing of RISC-V CPUs using Direct Instruction Injection

[2] The paper concludes that TestRIG accelerates development at all stages and provides a tighter debugging loop than the authors had experienced in any other processor development paradigm. Randomized Testing of RISC-V CPUs using Direct Instruction Injection

[3] A TestRIG generator found a memory-operation bug after 42 tests and 20 rounds of shrinking; the final counterexample had two loads and one store to overlapping addresses, was found less than 10 seconds into the run, and was fixed within the hour. Randomized Testing of RISC-V CPUs using Direct Instruction Injection

[4] The same bug had escaped the Flute processor development process, was not found by the RISC-V unit-test suite, and was overwhelmingly difficult to debug from a full software trace, but was trivial to resolve with a TestRIG counterexample. Randomized Testing of RISC-V CPUs using Direct Instruction Injection

[5] The CHERI extension to Ibex is presented as a striking example: after Ibex gained RVFI-DII support, a summer intern independently added full CHERI functionality in a month due to the tight cycle of reduced counterexamples from QCVEngine. Randomized Testing of RISC-V CPUs using Direct Instruction Injection