A formal engineer is fighting false counterexamples: the tool keeps finding traces where the producer pushes into a FIFO that is nearly full, and the downstream logic was never designed for that. The producer in this system never sends more than three words without a pop, so the engineer adds an assumption saying exactly that. The counterexamples disappear and every property passes. One of those properties was about the FIFO's full flag, which now can never be reached.

How do assumptions go wrong, and how do you catch it?

The obvious answer, and why it breaks

The obvious use of assumptions is to silence counterexamples until the proof passes. Each assumption removes input sequences from the proof. An assumption that matches a guarantee of the real environment removes only impossible traces. One that is stricter than the environment removes possible traces too, and with them the bugs they would have exposed. A passing proof cannot tell you which kind you wrote.

The idea: assumptions are a model of the environment

The same principle as constraints in simulation (lesson 4.3), with sharper consequences: an over-constrained random test still runs other cases, but an over-constrained proof reports proved for a property it never examined.

Build it: a false proof, and the cover that exposes it

This is lesson 7.2's buggy FIFO, with an assumption that pushes stop once three words are held:

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

// formal: bmc 12
// Lesson 7.4: an over-constrained proof. This is the buggy FIFO of lesson 7.2 (full rises one
// entry late), but the environment assumption says pushes stop once 3 words are held,
// "because our producer never sends more than 3". Every assertion passes: the assumption has
// removed the only inputs that reach the bug.
module fifo_over (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);
  always @(*) if (count >= 3'd3) assume (!push);   // the over-constraint
  always @(posedge clk) if (past) assert (count <= 3'd4);
endmodule

The bounded check passes, as its first line says: the property "occupancy never exceeds 4" is safe because the FIFO never gets past 3. Now ask the opposite question. A cover asks whether a situation can occur; written as an assertion of its negation, a passing check means it cannot:

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

// formal: bmc 12
// Lesson 7.4: the over-constraint exposed. A cover asks "can the FIFO ever be full?"; written
// as an assertion of the opposite, a passing bounded check means "never, within 12 cycles".
// It passes: under the assumption the FIFO never holds 4 words, so no check about full
// behaviour was ever exercised.
module fifo_cover (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);
  always @(*) if (count >= 3'd3) assume (!push);   // the over-constraint
  always @(posedge clk) if (past) assert (count != 3'd4);   // cover "full", negated
endmodule

It passes too, and that is the alarm: under the assumptions, the FIFO can never be full, so no property about full behaviour was ever exercised. Remove the over-constraint and lesson 7.2's counterexample comes straight back.

A real case: a feature silently ignored

While building lesson 7.9 for this course, the first plan put DCRouter's formal properties in a separate checker module attached with SystemVerilog bind. The proof passed, quickly. A deliberately false property also passed. The open-source Yosys version used here accepted the bind statement and ignored it: no property was checked at all. The properties were moved inside the design under ` ifdef FORMAL `` (fact V9), where a deliberately false one fails as it should. The lesson is the same as the FIFO's: a proof that has never failed has not shown that it checks anything.

Guarding against over-constraint

• Every assumption traces to the neighbour's specification, not to one neighbour's habit or to a counterexample you wanted gone.

• Cover the important situations: full, empty, every state, every grant; an unreachable cover means the proof is vacuous there.

• Plant a bug and expect a counterexample: as in lessons 7.2 and 7.9; if the proof still passes, it is not checking.

• Prefer assume-guarantee: assumptions about block A's inputs are proved as assertions on block B's outputs.

How real teams manage assumptions

What breaks

The opening story is the model above. The illustrative team's assumption came from the producer they had, not from the interface specification; a later producer sent four words, filled the FIFO, and met the late full flag in the lab. A cover on "FIFO full" would have shown the over-constraint the day it was written.

Key takeaways

• Assumptions model the environment: too few give false counterexamples, too many give false proofs.

• Over-constraint is silent; covers on key situations and planted bugs expose it.

• A proof that has never failed has not shown it checks anything.

Related topics

• Part 7 overview: Formal and Simulation