Counters and Clock Dividers

Counters and clock dividers look too simple to need formal verification, yet off-by-one errors in them are among the most common bugs in RTL. A divider that ticks every 4 cycles instead of 3 slows a UART or a timer by a third, and a simulation that only checks "a tick happens" never notices. This article writes the standard properties for a tick divider, finds an off-by-one bug, and proves the fixed design for every cycle.

8 min read | Intermediate

What You'll Learn

• Write the standard properties of a counter: range, wrap, step and period
• Measure the period of a tick with a helper counter
• Find an off-by-one bug in a clock divider
• Prove a counter property for every cycle with a helper invariant

Standard Counter Properties

• Range: the count stays within its legal values, cnt <= N - 1.
• Step: it changes only by the allowed amount, cnt == $past(cnt) + 1 or a wrap to 0.
• Wrap: it wraps exactly at the limit, $past(cnt) == N - 1 |-> cnt == 0.
• Period: an output pulse comes exactly every N cycles, no earlier and no later.
• Enable and hold: without the enable, the count does not change.

The period property is the one closest to the specification: it says what the user of the divider sees, without referring to the internal count at all.

The Design: a Tick Divider

This divider produces a one-cycle tick every N cycles, for example to run a slow peripheral from a fast clock:

module tick_div #(parameter N = 3) (input clk, input rst, output tick);
  reg [3:0] cnt;
  assign tick = (cnt == N - 1);
  always @(posedge clk)
    if (rst)                   cnt <= 4'd0;
    else if (cnt == N)         cnt <= 4'd0;     // bug: should wrap at N - 1
    else                       cnt <= cnt + 4'd1;
endmodule

The counter should run 0, 1, 2 and wrap. It wraps one value too late, so it also visits 3, and the ticks come every 4 cycles.

The Period Property

In SVA, "exactly N cycles between ticks" can be written as: after a tick, no tick for N - 1 cycles, then a tick.

a_period: assert property (@(posedge clk) disable iff (rst)
                           tick |=> !tick [*N-1] ##1 tick);

In the lab form, a helper counter gap measures the cycles since the last tick:

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // helper: cycles since the last tick (or since reset)
  reg [3:0] gap = 4'd0;
  always @(posedge clk) gap <= (rst || tick) ? 4'd1 : gap + 4'd1;
  // ticks are exactly N cycles apart
  always @(*) if (!init && tick && seen) assert (gap == N);
  // and never more than N cycles apart
  always @(*) if (!init) assert (gap <= N);
  reg seen = 1'b0;
  always @(posedge clk) if (!rst && tick) seen <= 1'b1; else if (rst) seen <= 1'b0;
`endif

The seen flag skips the first tick after reset, whose distance from reset is not a period. The run fails at step 7:

The first tick comes in step 3. The counter then visits 3, which it should never do, and the next tick comes in step 7, four cycles later. Change the wrap to cnt == N - 1 and the run passes.

Proving It for Every Cycle

A bounded run at depth 10 covers several periods, which is enough to trust this small design. As a proof, k-induction in prove mode returns UNKNOWN at first: the step starts from states where gap and cnt disagree, which reset never produces. One helper invariant ties them together:

// helper invariant for the induction proof
always @(*) if (!init && !rst) assert (gap == cnt + 4'd1 && cnt <= N - 1);

With it, the proof passes with k = 1. The PDR engine (abc pdr) proves the original properties without the helper. Both are shown in the strengthening invariants article for a different design.

Running It in ChipVerify Lab

The example below is the buggy divider with the period properties, at N = 3. It fails at step 7 within the free depth.

Common Mistakes