FIFO module assertion

SystemVerilog
, ,
1

Hello,

I need some help with assertions.

I have a fairly simple assertion for a FIFO module:

If FIFO is full and an attempt to write is made (but not read), write pointer does not change.

property fifofull;
    @(posedge clk) disable iff(reset)
    fifo_full && wr_en && !rd_en |=>  $stable(fifo_wr_ptr) ;
  endproperty

  fifofull_assert: assert property(fifofull) else 
    $display("fifofull assertion failed");

assertion_fail
assertion_fail1606×331 65.3 KB

The assertion failure message is where the red arrow is shown on the waves. When signals wr_en and fifo_full transition from 1 to 0, fifo_wr_ptr changes from 11 to 12 and assertion fires and fails.

I don’t see an actual issue with the DUT here; so how do I avoid the assertion failure here?

Thanks in advance.

2

The failure should occur in the clock cycle following the cycle when the antecedent is a match because of the |=> operator.

@(posedge clk) disable iff(reset)
    fifo_full && wr_en && !rd_en |=>  $stable(fifo_wr_ptr) ;

The assertion looks correct. Check the DUT; why if the fifo_wr_pntr incremented?
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.