A formal tool reports "PASSED" for a FIFO property. A reviewer asks the question that matters: passed for what? The answer is in the command line: depth 12. The tool considered every input sequence of up to 12 cycles after reset. A bug that needs 13 cycles to appear is outside the question it answered.

What does a bounded proof tell you, and what does it not?

The obvious answer, and why it breaks

The obvious reading of a passing formal check is "proved". A bounded check proves something narrower: no input sequence of length up to N, starting from reset, breaks the property. If every interesting state is reachable within N cycles, that is as good as a proof; if some are not (a counter that needs 255 events, a FIFO 64 deep, a timer of 1,000 cycles), the bounded check never looked at them.

The idea: unroll N cycles and ask the solver

• Unrolling: the tool makes N copies of the design's logic, one per cycle, connected through the registers, starting from the reset state (fact V2).

• The question: is there any assignment of the inputs in those N cycles that makes an assertion false in any of them, while every assumption holds?

• The answer: a counterexample of at most N cycles, usually the shortest, or a pass meaning "none within N".

• The cost: grows quickly with N and with the amount of state; it is a search, not a simulation.

Build it: a bounded proof of a FIFO

A 4-entry FIFO, with push, pop and data free: the solver considers every sequence of them. Three properties: occupancy never exceeds 4; full and empty agree with it; a refused push changes nothing. The run uses the course's open-source flow (Yosys with yosys-smtbmc and z3, fact V9).

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
27

// formal: bmc 12
// Lesson 7.2: a bounded proof of a 4-entry FIFO. push, pop and din are free: the solver
// considers every sequence of them for 12 cycles from reset. Properties: occupancy never
// exceeds 4, full and empty agree with it, and a refused push leaves the FIFO unchanged.
module fifo_bmc (input logic clk, rst, push, pop, input logic [7:0] din);
  logic [7:0] mem [0:3];
  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) begin mem[wp] <= din; wp <= wp + 2'd1; end
      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);               // reset in the first cycle only
  always @(posedge clk) if (past) begin
    assert (count <= 3'd4);
    assert (full == (count == 3'd4) && empty == (count == 3'd0));
    if ($past(push && full && !pop && !rst)) assert (count == $past(count) && wp == $past(wp));
  end
endmodule

The bounded check passes to depth 12. The same proof on a FIFO whose full flag rises one entry late:

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: bmc 12 expect fail
// Lesson 7.2: the same proof on a FIFO whose full flag rises one entry late. The solver
// returns a counterexample: the shortest input sequence that breaks a property.
module fifo_bmc_bug (input logic clk, rst, push, pop, input logic [7:0] din);
  logic [7:0] mem [0:3];
  logic [1:0] wp, rp;
  logic [2:0] count;
  logic full, empty;
  assign full  = (count > 3'd4);                   // BUG: should be (count == 4)
  assign empty = (count == 3'd0);
  always @(posedge clk)
    if (rst) begin wp <= 0; rp <= 0; count <= 0; end
    else begin
      if (push && !full) begin mem[wp] <= din; wp <= wp + 2'd1; end
      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);               // reset in the first cycle only
  always @(posedge clk) if (past) begin
    assert (count <= 3'd4);
    assert (full == (count == 3'd4) && empty == (count == 3'd0));
    if ($past(push && full && !pop && !rst)) assert (count == $past(count) && wp == $past(wp));
  end
endmodule

This one fails, as the first line says it should. The counterexample the solver returns is five steps long: reset, then four pushes with no pop; in step 5 the FIFO holds four words and full is still low, breaking "full agrees with occupancy". Compare lesson 1.3, where a simulation found the same bug only in a test that happened to push five times without popping. The solver found the shortest such test by itself.

Choosing a depth

Measured on DCRouter with its formal properties (lesson 7.9), one bounded check of the whole router took about 3 seconds at depth 6, 41 seconds at depth 8, and did not finish in five minutes at depth 10. Each extra cycle multiplies the search. DCRouter's FIFO-full bug needs at least 10 cycles (reset, eight words held, then a ninth push) and its credits-during-sleep bug at least 13 (a flit sent, eight idle cycles, sleep, then a credit returned), which is why lesson 7.9's depth-7 bounded check cannot see them; its full proof by induction can.

How real teams use bounded checks

What breaks

A team (illustrative) ran bounded checks to depth 20 on a 32-entry FIFO controller and reported all properties passed. The overflow logic could only be reached after 32 pushes. Depth 20 never filled the FIFO, so every property about full was vacuously safe within the bound. A parameterised 4-entry configuration (lesson 3.6) or an inductive proof would have reached it.

Key takeaways

• A bounded check proves no violation within N cycles of reset, and nothing beyond.

• Counterexamples are short, complete bug reports found without writing a test.

• Cost grows steeply with depth: justify the bound, and use induction or abstraction for deep state.

Related topics

• Part 7 overview: Formal and Simulation