Counterexample Generation

Concept

Counterexample generation is the process, illustrated in both UCLID5-based formal verification and model-checking-based directed test generation, of turning a satisfiable negated property into a concrete sequence of model actions that violates the intended property. In UCLID5, satisfiability results from an SMT solver are converted into counterexamples that help diagnose design errors, modeling inaccuracies or over-abstraction, and incorrectly stated verification conditions. In directed micro-architectural test generation, temporal logic properties are decomposed across partitioned modules and merged across clock steps so that the combined counterexample forms an executable test program.

First seen 5/26/2026

Last seen 7/3/2026

Evidence 4 chunks

Wiki v2

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 two 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]

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

decompositional model checking ← uses 95% 2e

Decompositional model checking uses counterexample generation to produce test programs

UCLID5 ← introduces 100% 1e

When a verification condition fails, UCLID5 generates a counterexample showing a sequence of actions that violate the condition.

LINKED ENTITIES

1 links

decompositional model checking USES Extracted graph relationship

CITATIONS

15 sources

15 citations — click to expand

[1] In the UCLID5 workflow, the SMT solver supplies concrete values for all data elements in the formula when satisfiable, and UCLID5 uses those values to construct a counterexample as a sequence of model actions that would violate a verification condition. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[2] UCLID5 generates verification conditions that are typically negations of the desired properties and invokes an SMT solver; in this work the Z3 solver was used (UCLID5 version 0.9.5, Z3 version 4.5.0). Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[3] The SMT solver can return unsatisfiable, satisfiable, or indeterminate outcomes, each with distinct implications for the verification condition. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[4] Generated counterexamples in the UCLID5 setting can indicate 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

[5] A general modeling rule in UCLID5 is to use the most abstract model that still captures the properties required for correctness, and counterexamples can reveal when abstraction is too coarse or inaccurate. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[6] In directed micro-architectural test generation, the negated property together with the processor model is applied to a model checker, which produces a counterexample containing a sequence of instructions (a test program) from an initial state to a failure state. Directed Micro-architectural Test Generation for an Industrial Processor: A Case Study

[7] The e500 processor model is partitioned into modules based on functional units 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] Properties for pipeline interactions are expressed in LTL using operators G, F, X, U and Boolean connectives, often in the form F(p1 ∧ p2 ∧ … ∧ pn) combining activities over n modules. Directed Micro-architectural Test Generation for an Industrial Processor: A Case Study

[9] Some property forms (e.g., F(p ∧ q), G(p ∨ q)) admit no simple decomposition, and others (e.g., pUq, F(p → F(q)), F(p → G(q))) are decomposable but not beneficial compared to traditional model checking. Directed Micro-architectural Test Generation for an Industrial Processor: A Case Study

[10] Boolean decompositions used 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(q). Directed Micro-architectural Test Generation for an Industrial Processor: A Case Study

[11] Introducing an explicit clock variable enables decompositions for counterexample generation that are not logically equivalent but yield 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

[12] Partial counterexamples from partitioned modules are integrated using clock-based merging; when two sub-properties share a parent module at clock ts, the counterexamples are merged into the parent's output property to generate counterexamples at clock ts − 1. Directed Micro-architectural Test Generation for an Industrial Processor: A Case Study

[13] In the e500 pipeline, counterexamples generated from multiple RS modules at cycle k are merged for the Issue stage; the negated merged property is applied with the Issue module to produce counterexamples at cycle k − 1, propagating back to Decode, GIQ, and Rename buffer. Directed Micro-architectural Test Generation for an Industrial Processor: A Case Study

[14] Concrete test programs generated by this approach include instruction dual issue (length 15), renaming src1 operand (length 12), reading operand from forwarding path for RAW (lengths 9 and 7), reading operand from renaming register for RAW (length 10), and reading operand from GPR for RAW (length 11). Directed Micro-architectural Test Generation for an Industrial Processor: A Case Study

[15] Decompositional model checking applies decomposed sub-properties to appropriate modules and merges their partial counterexamples to construct the final test program. Directed Micro-architectural Test Generation for an Industrial Processor: A Case Study