SVA 再了解(九)

SVA for Data Integrity in Asynchronous FIFO

int wcnt, rcnt;
always @(posedge wclk) if (write) wcnt = wcnt + 1;
always @(posedge rclk) if (read) rcnt = rcnt + 1;
property p_data_integrity;
int cnt;
logic data;
@(posedge wclk)
(write, cnt=wcnt, data=wdata) |=>
@(posedge rclk)
first_match(##[0:$] (read & (rcnt==cnt))) //$盡量不要用，會拖慢模擬速度
##0 (rdata==data);
endproperty

assert property (p_data_integrity);