Property for when writes to a fifo stop

Hi,

Unless the read signal was constant, IFV would fail this assertion as by simply alternating the value of write,

i.e. write 0 1 0 1 0 1 0 1 etc...

This would satisfy the assumption, but unless the FIFO was always being read, it would never reach an empty state.

Can you clarify the requirement here, for example when the write stops, do you never expect it to start again?
If this is the case then you would need another assumption, for example:

//psl assume_wr_never_restarts: assume always(
// {~write} |=> {~write}
//)@(posedge clk);


Vince.

Not quite. I want to say that writes will eventually completely stop and when they do the fifo should eventually empty.  There could be many stops and starts of the writes along the way.

I think the answer is to use an abort.

//psl assert_eventually_empty: assert always(
// {~empty} |-> {[*] ; empty}! abort (write)
//)@(posedge clk);

So, if writes stop, this assertion will check to make sure that the FIFO will evenutally become empty.

I don't think you can do this without some verilog code.
Look at this. I think it should work:


`ifdef FORMAL_ON

reg [SIZE-1:0] num_write;
reg [SIZE-1:0] cnt_write;


// Let the formal tool pick a value for num_write and keep it stable
// psl assume_num_write_stable : assume always (stable(num_write));

// Count numbers of write
always @(posedge clk)
begin
if (reset)
cnt_write <= 0;
else if (write)
cnt_write <= cnt_write+1'b1;
else
cnt_write <= cnt_write;
end

// if numbers of writes reaches num_write, don't generate any writes anymore
//psl assume_max_write : assume always ((cnt_write == num_write) -> (~write) @(posedge clk);

// Force number of write equal to num_write. This will force write to be asserted
//psl assume_write: assume always (eventually! cnt_write == num_write) @(posedge clk);

// force read to be asserted. If not, the fifo will never go empty
// psl assume_read: assume always (eventually! read) @(posedge clk);

// the fifo should eventually be empty
//psl assert_empty: assert always (eventually! empty) @(posedge clk);

`endif FORMAL_ON

Claude

Hi Claude,

Thanks for the reply.  Did you see my last post?  Do you think there is still a problem doing it the way I mention?  If so, can you explain?  Thanks.

Also, your code puts an assumption on the read.  However, my example was describing a case where the logic being verified is what is reading the fifo.  I am verifying that the logic does indeed empty the fifo if writes stop.

Ross

Ross,

Yes your solution works fine and is much more elegant than mine!! I tried both solution on some fifo code I had. Both worked.
I did have to add the constraint on read because I considered as an input to the fifo block.

Thanks,

Claude