Assertions for asynchronous FIFO

Assertions for asynchronous FIFO

Scenario 1

- If FIFO is empty, read_pointer does not change

property check_empty;
@(posedge rclk) disable iff(rclk_rst)
fifo_empty |-> @(posedge rclk) 
if(!unknown($past(read_pointer)))
read_pointer === $past(read_pointer); 
endproperty

Scenario 2
- If FIFO is full, write_pointer does not change

property check_full;
@(posedge wclk) disable iff(wclk_rst)
fifo_full |-> @(posedge wclk) write_pointer === $past(write_pointer);
endproperty

Scenario 3
- Check that data that is read when read_pointer reaches write_pointer is same as the data that is written at the write_pointer

sequence read_detect(pointer);
##[0:$] (fifo_read && !fifo_empty && read_pointer === pointer); 
endsequence

property write_read_data_integrity_check;

integer pointer, data;

@(posedge wclk) disable iff (wclk_rst) || (rclk_rst)

fifo_write && !fifo_full, data = fifo_data_in, pointer = write_pointer)
->
@(posedge rclk) first_match(read_detect(pointer)) 

##0

fifo_data_out === data;

endproperty