A FIFO's designer writes a simple property: when the FIFO is empty, the read and write pointers are equal. It is true; every bounded check passes, at every depth anyone tries. Then the formal tool is asked for a full proof, and it returns a counterexample to the induction step: a FIFO with a count of 1 and equal pointers, which pops and ends up empty with unequal pointers. No such FIFO can exist. The tool knows that only if someone tells it.

How do you prove a property for all depths, and why does a true property sometimes fail?

The obvious answer, and why it breaks

The obvious path to a full proof is a very deep bounded check. No depth is enough for a design that can run forever, and cost grows steeply (lesson 7.2). Induction avoids the bound, but it reasons from arbitrary states, including states the design can never reach. A property that holds in every reachable state can fail from an unreachable one, and then the proof is inconclusive until the unreachable states are ruled out.

The idea: base case and induction step

A helper invariant is an extra property, true in every reachable state, that rules out the unreachable states the induction step would start from. It must itself be proved, which is why it is written as an assertion, not an assumption.

Build it: the same property, without and with a helper

The FIFO keeps its count and its pointers in separate registers. Without help, induction is allowed to start from count 1 with equal pointers:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

// formal: prove 4 expect unproven
// Lesson 7.3: induction without a helper invariant. The FIFO keeps its count and its pointers
// separately. The property "empty means the pointers are equal" holds in every reachable
// state, so the bounded check passes, but induction can start from an unreachable state
// (count 1 with equal pointers) where one pop breaks it.
module fifo_ind (input logic clk, rst, push, pop);
  logic [1:0] wp, rp;
  logic [2:0] count;
  logic full, empty;
  assign full  = (count == 3'd4);
  assign empty = (count == 3'd0);
  always @(posedge clk)
    if (rst) begin wp <= 0; rp <= 0; count <= 0; end
    else begin
      if (push && !full) wp <= wp + 2'd1;
      if (pop && !empty) rp <= rp + 2'd1;
      count <= count + 3'(push && !full) - 3'(pop && !empty);
    end
  logic past = 1'b0;
  always @(posedge clk) past <= 1'b1;
  always @(*) assume (rst == !past);
  always @(posedge clk) if (past && !rst) assert (!empty || wp == rp);
endmodule

The first line says what happens, and the course's checker confirms it: the bounded check passes and the induction step fails. Now with a helper invariant, "the count equals the distance between the pointers, and is at most 4":

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26

// formal: prove 4
// Lesson 7.3: the same proof with a helper invariant tying the count to the pointers. The FIFO keeps its count and its pointers
// separately. Without help, induction can start from an unreachable state (count 1 with
// equal pointers). With the helper invariant asserted, those states are excluded and both
// the base case and the induction step pass.
module fifo_ind_helper (input logic clk, rst, push, pop);
  logic [1:0] wp, rp;
  logic [2:0] count;
  logic full, empty;
  assign full  = (count == 3'd4);
  assign empty = (count == 3'd0);
  always @(posedge clk)
    if (rst) begin wp <= 0; rp <= 0; count <= 0; end
    else begin
      if (push && !full) wp <= wp + 2'd1;
      if (pop && !empty) rp <= rp + 2'd1;
      count <= count + 3'(push && !full) - 3'(pop && !empty);
    end
  logic past = 1'b0;
  always @(posedge clk) past <= 1'b1;
  always @(*) assume (rst == !past);
  always @(posedge clk) if (past && !rst) begin
    assert (!empty || wp == rp);                   // the property
    assert (count <= 3'd4 && count[1:0] == 2'(wp - rp));   // the helper invariant
  end
endmodule

Both the base case and the induction step pass: the property is proved for every depth. The helper ruled out every state where count and pointers disagree, and in all remaining states one more cycle preserves the property. Note that the helper is what a designer would call the FIFO's defining relationship; DCRouter's FIFO carries the same invariant in its formal properties, and with it the whole router's FIFO, arbiter and credit properties are proved by a 4-step induction (lesson 7.9).

When induction fails

• Read the induction counterexample's first state: if it cannot happen in reality, write the invariant that forbids it.

• Typical helpers: counters agree with pointers; one-hot states are one-hot; a lock implies an owner; credits plus outstanding items equal the total.

• Increase k: a larger induction depth rules out states that cannot persist for k cycles, at higher cost.

• Suspect a real bug: a failing step can also start from a reachable state deeper than the base case; check reachability before writing a helper.

How real teams get full proofs

What breaks

A team (illustrative) made a stubborn induction pass by writing the missing relationship as an assumption instead of an assertion. The proof passed. The assumption was false in one corner of the design, so it had silently removed real behaviour from the proof, and a bug lived there. Helpers must be asserted and proved; assuming them is over-constraining (lesson 7.4).

Key takeaways

• Induction proves a property at every depth: base case from reset, step from any state.

• A true property can fail induction from an unreachable state; a helper invariant rules such states out.

• Helpers must be asserted and proved, never assumed.

Related topics

• Part 7 overview: Formal and Simulation

• Formal course: Property Development