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
Link to the list of papers and books that I wrote, many are now donated.
http://systemverilog.us/vf/Cohen_Links_to_papers_books.pdf
or
https://rb.gy/ibks5p
Getting started with verification with SystemVerilog
https://rb.gy/f3zhh
