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]

In the directed micro-architectural test generation setting, the negated version of a desired property together with the processor model is applied to a model checker, which automatically produces a counterexample that contains a sequence of instructions (a test program) leading from an initial state to a failure state. [mtv06-test-generation-from-counterexample]

In the ADL-driven functional test program generation setting using SMV, designers write properties by hand specifying the negation of the behavior they want to validate; the SMV model checker then produces a counterexample in the form of an instruction sequence, which is converted into a complete test (instruction sequence plus expected results) by a cycle-accurate structural simulator generated from the Architecture Description Language (ADL) specification. [adl-smv-counterexample]

Role in a UCLID5 Verification Flow

Given a model and verification script, UCLID5 generates verification conditions as formulas in logics that support the theories used by the model. These formulas are typically negations of the properties the user wants to verify, and UCLID5 invokes an SMT solver to analyze them. [verification-condition-generation]

The solver can return three outcomes:

• Unsatisfiable: because the checked formula is typically the negation of the property, unsatisfiability indicates that the desired verification condition holds.
• Satisfiable: the solver provides concrete satisfying values, which typically implies that some verification condition failed; these values are used for counterexample generation.
• Indeterminate: the solver cannot find a satisfying solution but also cannot prove unsatisfiability, which typically indicates that the model is too complex or needs reasoning beyond what the solver can provide. [solver-outcomes]

Diagnostic Meaning

A generated counterexample is not automatically proof of a design bug alone. In the cited UCLID5 setting, counterexamples are important indications of one of three situations: a true error in the design, an inaccurate or overly abstract model, or an improperly expressed verification condition. [counterexample-diagnostics]

Interaction with Abstraction

The UCLID5 evidence emphasizes that formal models involve choices about data types and abstraction level. A general rule stated for the UCLID5 modeling context is to use the most abstract model that still captures the properties required for correctness. Counterexamples can therefore serve as feedback not only about the implementation being modeled, but also about whether the abstraction is too coarse or otherwise inaccurate. [model-abstraction]

Example Context from the Evidence

The cited UCLID5 report applies this workflow to formal verification of pipelined Y86-64 microprocessors, using the Z3 SMT solver (UCLID5 version 0.9.5 and Z3 version 4.5.0). [uclid5-z3-context]

Counterexample Generation as ADL-Driven Functional Test Generation (SMV)

In the cited ADL-driven approach, the designer starts by specifying the microprocessor architecture in an Architecture Description Language (ADL); the processor model is generated automatically from this ADL specification and described in the SMV language. The verification engineer writes properties by hand in SMV (specifically, the negation of the property that should hold). The SMV model checker is applied to the model with these negated properties and produces a counterexample in the form of an instruction sequence that activates the targeted behavior. Each counterexample is then combined with the expected results produced by a cycle-accurate structural simulator (also generated automatically from the ADL specification) to yield a complete functional test. Coverage reports from the simulator drive the addition of new properties when coverage is insufficient. [adl-smv-overview]

Two concrete examples from this setting illustrate the workflow:

• A property hazard: assert G(ID._stall = 0); is used to generate a counterexample that stalls the decode unit via a read-after-write hazard. The property is negated and applied to the SMV model; the SMV model checker returns an instruction sequence (NOP, ADD R3,R1,R2, ADD R4,R3,R2) that exercises the stall at cycle 4. The reported run time was 1.3 seconds on a 359 MHz Sun UltraSPARC-II with 2048M RAM. [adl-smv-stall-example]
• A property init: assert G((cycle = 8) -> X((DIV.Ain != 2) | (DIV.Bin != 3))); is added to drive a previously uncovered path in the division unit by initializing internal registers Ain and Bin to values 2 and 3 at clock cycle 9. The model checker produces a counterexample (NOPs followed by MOVI R4,#2; MOVI R5,#3; DIV R0,R4,R5) in 75.4 seconds on the same platform. [adl-smv-div-example]

The cited approach explicitly states that it pursues this direction because functional verification consumes a significant portion of the microprocessor design cycle, and model checking offers an opportunity to reduce validation cost. Future work identified in this report includes applying the resulting tests to the RTL description of the processor, automatic coverage estimation, and automatic generation of properties from the ADL specification. The authors also note that they are investigating the use of SAT-based bounded model checkers to generate functional test programs. [adl-smv-summary]

Counterexample Generation as Directed Test Generation (e500 Pipeline)

In the directed micro-architectural test generation work on the e500 superscalar processor (Power Architecture Technology), counterexample generation is repurposed as test-program generation. The processor model is partitioned into multiple modules based on functional units (e.g., reservation stations, issue, decode, GIQ, rename buffer), because verifying the whole model as a single unit is infeasible due to state explosion during model checking. [mtv06-model-partitioning]

Properties expressed in Linear Temporal Logic (LTL) using operators G, F, X, U combined with Boolean connectives ∧, ∨, ¬, → are generated from pipeline interactions and negated so that a counterexample represents an interaction fault. A common pattern is F(p1 ∧ p2 ∧ … ∧ pn), expressing that activities pi over n modules must become true at some time step. [mtv06-ltl-properties]

Naively checking the negated property against the whole model is unsuitable because of state explosion. To counter this, the cited approach decomposes properties across modules and uses decompositional model checking, in which sub-properties are applied to appropriate modules and partial counterexamples are merged to construct a final test program. [mtv06-decompositional-mc]

Property Decomposition for Counterexample Generation

Simple decompositions enabled by the Boolean structure of properties include:

• G(p ∧ q) = G(p) ∧ G(q)
• F(p ∨ q) = F(p) ∨ F(q)
• X(p ∨ q) = X(p) ∨ X(q)
• X(p ∧ q) = X(p) ∧ X(p)

Some combinations are not decomposable at all, for example F(p ∧ q) = F(p) ∧ F(q) and G(p ∨ q) = G(p) ∨ G(q). Other combinations such as pUq, F(p → F(q)), or F(p → G(q)) are decomposable in principle but the decomposition is not beneficial compared to traditional model checking. [mtv06-decomposition-rules]

Introducing an explicit clock (time step) variable clk and a specific time step ts into the property enables additional decompositions that are useful for counterexample generation. Although the left- and right-hand sides of these decompositions are not logically equivalent, they produce functionally equivalent counterexamples. An example is:

G((clk = ts) ∨ (p ∨ q)) ≈ G((clk = ts) ∨ p) ∨ G((clk = ts) ∨ q) [mtv06-clock-based-decomposition]

Merging Partial Counterexamples

A key challenge is integrating partial counterexamples generated for partitioned modules, because the relationships among decomposed modules and sub-properties are not generally preserved at the whole-design level. The cited approach proposes clock-based integration of partial counterexamples: when two sub-properties are applied at the same clock cycle (clk = ts) to two modules sharing a parent module, the two generated counterexamples are merged into the output property of the parent module, which is then used to generate counterexamples at the previous clock cycle (clk = ts − 1). [mtv06-merge-partial-cxes]

In the e500 pipeline, for instance, four reservation station (RS) modules share the Issue stage as a parent module; counterexamples generated from multiple RS modules at cycle k are merged into the output property of the Issue stage at cycle k, and the negated version of that property is applied to the model checker together with the Issue module to generate a counterexample at cycle k − 1 that produces the output properties of Decode, GIQ, and Rename buffer. Merging continues until the primary input instruction sequence is obtained. [mtv06-merge-example]

Produced Test Programs

The approach was applied to a set of interaction faults and corner cases, producing concrete test programs of the following kinds, with associated test code lengths:

[mtv06-test-cases]