Counterexample (trace)
Beginner
A step-by-step recipe, found by a proof tool, that makes the design break a rule.
Novice
What a formal tool returns when a rule can be broken: a specific sequence of inputs, clock cycle by clock cycle, that leads from start-up to the failure. Engineers replay it like a failing test.
Expert
Usually written out as a waveform or a small testbench. Bounded model checking returns the shortest one. A “counterexample” from the step of an induction proof that does not start from a reachable state is not a bug; it means the proof needs strengthening.
Explained in Verification (Design Flow).
See also: Formal verification, Bounded model checking (BMC).