Debugging counterexamples

Every counterexample has exactly one of three root causes. Asking the questions in order saves a lot of time:

Practical debugging techniques

• Read the trace backwards. Start at the failing cycle and ask which signal values made the property fail, then why each of them had that value one cycle earlier.
• Add signals generously. Internal state (FSM state, counters, pointers) explains most traces.
• Ask "what if" questions with covers. "Can this fail without stop ever being high?" — add !stop as a temporary assumption or cover the failure condition with extra constraints.
• Minimise first. Most tools can shorten a trace or make inputs "quiet" (fewer toggles). Simpler traces are easier to read.
• Never fix a failure by adding an assumption you cannot justify. Write down the source of every assumption.