Lesson 9.2 · When Proofs Lie: Avoiding False Positives

Over-constraining assumptions

Here is an up/down counter with a bug that only shows when up and down arrive in the same cycle.

updown.sv

// updown.sv — counter with a bug for simultaneous up/down
module updown (
  input  logic       clk, rst, up, down,
  output logic [3:0] cnt
);
  always_ff @(posedge clk) begin
    if (rst)       cnt <= 4'd0;
    else if (up)   cnt <= cnt + 4'd1;     // BUG: up && down should leave cnt unchanged
    else if (down) cnt <= cnt - 4'd1;
  end
endmodule

updown_fv.sv

// updown_fv.sv — shows how an over-constraint hides the bug
module updown_fv (input logic clk, rst, up, down);
  logic [3:0] cnt;
  updown dut (.*);

  initial assume (rst);
  default clocking cb @(posedge clk); endclocking
  default disable iff (rst);

  // "Upstream never does both" -- convenient, but is it TRUE?
  m_not_both: assume property (!(up && down));

  a_both_hold: assert property (up && down |=> $stable(cnt));   // PROVEN... vacuously
  a_up:        assert property (up && !down |=> cnt == $past(cnt) + 4'd1);
  a_down:      assert property (down && !up |=> cnt == $past(cnt) - 4'd1);

  // The defence: cover the antecedents
  c_both:      cover property (up && down);                        // UNREACHABLE -> red flag
endmodule

All three assertions prove. But c_both is unreachable, which tells you that a_both_hold never checked anything. Remove m_not_both (or confirm with the upstream designer that both can happen) and a_both_hold fails immediately.

Where over-constraints come from

Convenience: an assumption added to silence a failure without understanding it.
Copy-paste: assumptions reused from another block whose environment was different.
Temporary steering from exploration (Chapter 5) left in by accident.
Assumptions on outputs or internal signals of the design — these constrain the very logic you are trying to check.
Contradictions: two assumptions that cannot both hold at some point, which removes every trace beyond it. Tools report this as "assumptions conflict" or "dead-end" — never ignore it.