Clock-based Counterexample Integration

Clock-based counterexample integration is a method used during the directed micro-architectural test generation of an industrial processor. It addresses a central challenge of decompositional model checking: after a processor model is split into structure-oriented modules (e.g., reservation stations, issue, decode, GIQ, rename buffer) and sub-properties are checked independently, the partial counterexamples produced for those modules must be combined into a single counterexample that is valid for the whole design.

Motivation

In decompositional model checking the relationships among decomposed modules and their corresponding sub-properties are not, in general, preserved at the whole-design level. Each module's model checker produces a counterexample that explains a local violation, but these traces must be merged so that a global counterexample can drive test-program generation. Naive merging can misalign the partial traces because the modules operate at different positions in the pipeline.

Core Idea

The technique proposed in the MTV'06 case study uses the clock cycle (clk) of the underlying model as the alignment axis. The variable clk counts time steps, and ts denotes a specific time step in the counterexample trace.

• When two or more sub-properties are applied at the same clock cycle (clk = ts) to modules that share a parent module, the corresponding partial counterexamples are merged.
• The merged counterexample then becomes the output property of the parent module, evaluated at the previous clock cycle (clk = ts − 1).
• This parent-level counterexample is, in turn, used to derive output properties for the parent's own predecessors, and the merging continues upward until the primary inputs of the design are reached.

Worked Example

In the processor model described in the paper:

1. Four reservation station (RS) modules share the parent module Issue.
2. Counterexamples generated from the multiple RS modules at cycle k are merged to construct the output property of the Issue stage.
3. The negated form of this merged property is fed to the model checker together with the Issue module to produce a counterexample at cycle k − 1.
4. That counterexample is then used to derive the output properties of Decode, GIQ, and Rename buffer.
5. The process continues iteratively until the trace reaches the primary inputs of the design, yielding a complete counterexample trace.

Role in the Test Generation Flow

Clock-based counterexample integration sits between partial counterexample generation (per module) and final test-program synthesis. By aligning partial counterexamples along the common clock cycle, the method enables the composition of local violations into a single, end-to-end micro-architectural test. The resulting tests exercise pipeline interactions such as dual issue, operand renaming, and various RAW read-after-write forwarding scenarios (e.g., reads from the forwarding path, the renaming register, or the GPR).

Properties

• Generic: the framework is not tied to a specific pipeline and can be applied to industrial-strength processor models.
• Structure-driven: it exploits the structure-oriented decomposition of the processor model and the parent–child relationships among pipeline modules.
• Cycle-aligned: all merging steps are keyed on the discrete clock cycles produced by the model checker.

Limitations

Because module decompositions and sub-properties do not, in general, preserve their relationships at the whole-design level, alignment by clock cycle alone does not guarantee semantic equivalence to a monolithic counterexample. The technique relies on the assumption that sub-properties applied at the same clk value correspond to co-occurring pipeline interactions that can be legitimately merged at the parent module one cycle earlier.