Intro: Assertion Debug Problem

You have the following property intended to catch FIFO overflow:

property no_overflow;
  @(posedge clk)
    disable iff (!rst_n)
    !(fifo_full && fifo_push);
endproperty

assert property (no_overflow);

CopyEdit

property no_overflow; @(posedge clk) disable iff (!rst_n) !(fifo_full && fifo_push); endproperty assert property (no_overflow);

🔥 The assertion is firing during simulation.

Context:

• The fifo_full signal is generated inside the DUT.

• The fifo_push signal comes from the testbench (driven synchronously with clk).

• Reset (rst_n) is correctly asserted at time 0 and deasserted later.

• You're seeing the assertion fire right after reset deassertion.

❓ Your Job:

• What are 3 possible reasons this assertion could be falsely firing?

• What debug steps would you take to isolate the issue?

• How would you fix or re-write the assertion (if needed)?