Counterexample Generation
ConceptCounterexample generation is the activity of turning the satisfiable result of checking a negated property into a concrete artifact that witnesses how the property can be violated. In the UCLID5 setting, an SMT solver's satisfying assignment is converted into a counterexample that diagnoses design, modeling, or specification problems. In directed micro-architectural test generation and ADL-driven functional test generation for microprocessors, the same mechanism is repurposed so that counterexamples become concrete test programs (instruction sequences), built by decomposing properties across partitioned modules and merging the partial counterexamples back together. In stochastic and theorem-proving contexts, the notion is extended to collections of violating paths with sufficient probability and to example-driven diagnosis of failed conjectures.
First seen 5/26/2026
Last seen 9/5/2026
Evidence 10 chunks
Wiki v3
WIKI
Definition
Counterexample generation is the activity of turning the satisfiable result of checking a negated property into a concrete artifact that witnesses how the property can be violated. The cited evidence describes several distinct settings in which this notion appears.
In the UCLID5 setting, the workflow checks a verification condition by asking an SMT solver to satisfy the negation of the desired property; when the solver returns that the formula is satisfiable, it supplies concrete values for all data elements in the formula, including uninterpreted functions, and UCLID5 uses those values to construct a counterexample: a sequence of actions that could occur in the model and violate a verification condition. [counterexample-generation-from-satisfiability]
NEIGHBORHOOD
2 nodes · 1 edgesgraph · Counterexample Generation · depth=1
RELATIONSHIPS
5 connectionsDecompositional model checking uses counterexample generation to produce test programs
Registered Report: Generating Test Suites for GPU Instruction Sets through Mutation and Equivalence Checking ← uses 100% 2e
The paper uses counterexamples from CBMC to build the test suite.
Architecture Description Language driven Functional Test Program Generation for Microprocessors using SMV ← uses 100% 2e
The paper uses counterexamples generated by SMV as functional test programs
Test programs are generated as counterexamples from the model checker
When a verification condition fails, UCLID5 generates a counterexample showing a sequence of actions that violate the condition.
CITATIONS
17 sources17 citations — click to expand
[1] Counterexample generation converts the satisfiable result of a negated property check into a concrete witnessing artifact (UCLID5: a sequence of model actions; ADL/SMV and directed micro-architectural test generation: an instruction sequence that becomes a test program). Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[2] In UCLID5, when the SMT solver returns satisfiable, it provides concrete values for all data elements (including uninterpreted functions) and UCLID5 uses them to generate a counterexample: a sequence of actions that could occur in the model and violate a verification condition. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[3] UCLID5-generated counterexamples are diagnostic signals indicating a true design error, an inaccurate or overly abstract model, or an improperly expressed verification condition. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[4] UCLID5 invokes an SMT solver on the negation of the properties to verify; the solver can return unsatisfiable (desired verification condition holds), satisfiable (typically implies a verification condition failed; values used for counterexample generation), or indeterminate (model is too complex or requires reasoning beyond the solver). Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[5] Counterexample generation supports feedback on abstraction choices: as a general rule, the most abstract model that still captures the relevant correctness properties should be used, and counterexamples can reveal whether the abstraction is too coarse or inaccurate. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[6] In the directed micro-architectural test generation setting, the negated version of a desired property together with the processor model is applied to the model checker, which automatically produces a counterexample containing a sequence of instructions (a test program) from an initial state to a failure state; a naive whole-model approach is unsuitable due to state explosion. Directed Micro-architectural Test Generation for an Industrial Processor: A Case Study
[7] The e500 processor model is partitioned into multiple modules based on functional units (reservation stations, issue, decode, GIQ, rename buffer) because verifying the entire model as a single unit is infeasible due to state explosion during model checking. Directed Micro-architectural Test Generation for an Industrial Processor: A Case Study
[8] Pipeline interactions are expressed as LTL properties using temporal operators G, F, X, U and Boolean connectives ∧, ∨, ¬, →; a common pattern is F(p1 ∧ p2 ∧ … ∧ pn), expressing that activities pi over n modules must become true at some time step, and the negation is used so that the counterexample represents an interaction fault. Directed Micro-architectural Test Generation for an Industrial Processor: A Case Study
[9] Boolean decompositions useful for counterexample generation include G(p ∧ q) = G(p) ∧ G(q), F(p ∨ q) = F(p) ∨ F(q), X(p ∨ q) = X(p) ∨ X(q), and X(p ∧ q) = X(p) ∧ X(p); non-decomposable combinations include F(p ∧ q) = F(p) ∧ F(q) and G(p ∨ q) = G(p) ∨ G(q); combinations such as pUq, F(p → F(q)), or F(p → G(q)) are decomposable in principle but not beneficial compared to traditional model checking. Directed Micro-architectural Test Generation for an Industrial Processor: A Case Study
[10] Introducing a clock (time step) variable clk and a specific time step ts enables additional decompositions useful for counterexample generation; the sides are not logically equivalent but produce functionally equivalent counterexamples, e.g., G((clk = ts) ∨ (p ∨ q)) ≈ G((clk = ts) ∨ p) ∨ G((clk = ts) ∨ q). Directed Micro-architectural Test Generation for an Industrial Processor: A Case Study
[11] Partial counterexamples generated for partitioned modules are integrated using clock-based integration: when two sub-properties are applied at the same clock cycle (clk = ts) to two modules sharing a parent module, the two counterexamples are merged into the output property of the parent module and used to generate counterexamples at clk = ts − 1; merging continues until the primary input instruction sequence is obtained. Directed Micro-architectural Test Generation for an Industrial Processor: A Case Study
[12] In the e500 pipeline, four reservation station (RS) modules share the Issue stage as a parent module; counterexamples from multiple RS modules at cycle k are merged into the output property of the Issue stage, and the negated version of that property is applied with the Issue module to produce a counterexample at cycle k − 1 covering Decode, GIQ, and Rename buffer. Directed Micro-architectural Test Generation for an Industrial Processor: A Case Study
[13] The directed micro-architectural test generation approach produced concrete test programs for interaction faults and corner cases, with associated test code lengths: instruction dual issue (15), renaming src1 operand (12), read operand from forwarding path RAW (9), reservation station reads operand from forwarding path RAW (7), read operand from renaming reg. RAW (10), read operand from GPR RAW (11). Directed Micro-architectural Test Generation for an Industrial Processor: A Case Study
[14] In the ADL/SMV approach, the processor model is generated from the ADL specification and described in SMV; properties are written by hand as the negation of the desired behavior and applied with the SMV model checker to generate counterexamples (instruction sequences), which are combined with expected results from a cycle-accurate structural simulator (also generated from the ADL) to produce complete functional tests. Architecture Description Language driven Functional Test Program Generation for Microprocessors using SMV
[15] Applying the negated hazard property G(ID._stall = 0) to the SMV model of the DLX pipeline produces a counterexample in the form of an instruction sequence (NOP, ADD R3,R1,R2, ADD R4,R3,R2) that stalls the decode unit at cycle 4; SMV takes 1.3 seconds on a 359 MHz Sun UltraSPARC-II with 2048M RAM. Architecture Description Language driven Functional Test Program Generation for Microprocessors using SMV
[16] Adding the property init: assert G((cycle = 8) -> X((DIV.Ain != 2) | (DIV.Bin != 3))) generates a counterexample (MOVI R4,#2; MOVI R5,#3; DIV R0,R4,R5) that initializes the DIV unit internal registers Ain and Bin at clock cycle 9, exercising a previously uncovered path; SMV takes 75.4 seconds on a 359 MHz Sun UltraSPARC-II with 2048M RAM. Architecture Description Language driven Functional Test Program Generation for Microprocessors using SMV
[17] The ADL/SMV report frames functional verification as a significant cost driver in microprocessor design and pursues model checking as a way to reduce validation cost; future work includes applying tests to RTL, automatic coverage estimation, automatic generation of properties from the ADL specification, and investigating SAT-based bounded model checking for generating functional test programs. Architecture Description Language driven Functional Test Program Generation for Microprocessors using SMV