How to check data integrity with assertions?

Hi bijitm,

there is an example for data integrity in a fifo: If data enters the FIFO then “sooner or later” the same data exits the FIFO:

output_data_integrity : assert forall dvalue in {0:255} :
always ( (push && data_in == dvalue) ->
eventually! (pop && data_out == dvalue));

Two key aspects here are liveness (eventually) and non deterministic constants (forall). For a bus system this concept is also applicable, but maybe you are able to predict exactly when the output should show the data coming in (e.g. same or next cycle instead of eventually). The "push" in a bus system represents the control signal condition indicating a transfer coming in and the "pop" goint out.

In fully symmetric datapath a valid abstraction is to use only one bit instead of the full data vector, that can reduce complexity for the formal prove.

Joerg.

Hi!

Below is anoter way to do it without the forall.

logic [W-1:0] dvalue;
assume_stable_dvalue: assume always(stable(dvalue))@(posedge clk);

assert_data_integrity: assert always(
  push & (data_in==dvalue) ->eventually!
  pop & (data_out==dvalue)
)@(posedge clk);