How to assert that in the detection of FIFO, after sending data, it ends up being empty？

SystemVerilog
, ,
1

How to assert that in the detection of FIFO, after sending data, it ends up being empty？

2

In reply to ader:
From my Real CHip book ($3 at Amazon)
3.5.5.2 FIFO Full and Empty A FIFO is full when both pointers are equal. A FIFO is also empty when both pointers are equal, so the FIFO pointers should be one bit larger than is necessary to address the full memory range. The extra bit is used as a flag to help determine if the FIFO is empty or full. If the extra, pointer MSBs are equal, it means that the FIFO pointers have wrapped back to address 0 an equal number of times and if the rest of the FIFO bits are equal, the FIFO is empty. If the extra, pointer MSBs are not equal, it means that the write pointer has wrapped back to address 0 one more time than the read pointer and if the rest of the FIFO bits are equal, the FIFO is full.

From my SVA book, the support logic computes the full.empty

always @ (posedge clk)
  begin : status_flag
    fifo_is_empty = (wr_ptr == rd_ptr);
    fifo_is_full = (wr_ptr - rd_ptr) == FULL;

...
task push_task (word_t data);
     begin
       $display ("%0t %m Push data %0h ", $time, data);
	   data_in <= data;
	   push <= 1'b1;
	   pop  <= 1'b0;
       	   wr_ptr++;
	   ##1;
      end
    endtask : push_task 

    task pop_task;
      begin
        data_in <= 'X; // unsized Xs 
        push <= 1'b0;
        pop  <= 1'b1;
        rd_ptr++;
        ##1;
       end
    endtask : pop_task

You can then compare the RTL status against the predicted status with simple assertions.
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Cohen_Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog