Counter debugging and minimal counterexamples

A correct final value can hide an incorrect sequence

Ending at 0 does not establish correct reset and wraparound. A circuit stuck at 0 produces the same final value. Use observation points that separately expose normal incrementing, holding, reset^{iReset A control that returns state to a specified initial value. Define whether it is synchronous or asynchronous and whether it has priority over other controls. Learn more} and boundary wraparound.

Deliberately combine conflicting controls

Priority errors are hard to find when controls are tested only separately.

Each column below records a rising edge^{iRising edge The instant at which the clock changes from 0 to 1. Distinguish it from a level, which refers to the entire interval during which CLK=1. Learn more}. Inputs are pre-edge; states labeled “after” are post-update. Alignment denotes sample order, not physical propagation delay^{iPropagation delay The time from an input change until the output settles to the correct value. Logical equivalence and timing behavior are separate properties. Learn more}. Initially count=5. The faulty circuit checks reset only inside enable and therefore holds 5 at the first edge. Although the final values agree, the first mismatch reveals the fault.

Start the modulo-8 reference circuit at 101. Select enable=0 and reset=1, then advance the clock. The correct value is 000; RTL that places reset inside enable holds 101. Release reset and also distinguish holding with enable=0 from incrementing with enable=1.

Find the first mismatch with a reference model

This functional model assumes valid states 0–M-1. Add a separate policy for out-of-range recovery. Compute and compare the expected value at each edge. Inputs and state immediately before the first mismatch are the smallest useful starting point for diagnosis.

If failure appears after 1000 cycles, remove unnecessary input intervals to reproduce it in three to five edges. After fixing RTL, retain that minimal counterexample as a regression test. Review the revised specification and code separately so that the design and test are not both changed to the same incorrect condition.