Assertion modelling using time delay

In reply to ben@SystemVerilog.us:

Problem Statement: When Signal A is de-asserted (from 0 to 1)
and within 700ns Signal B should be de-asserted (from 1 to 0).
This property should be re-usuable.


// minor corrected Code:
property delay (logic a,b, realtime delay);
realtime t_v[2];
@(posedge a)(1, t_var[0] = $realtime) ##0 @(negedge b)(1, t_v[1] = $realtime) ##0(t_v[1] - t_v[0]) <= delay;
endproperty
delay_s1    : assert property (@(posedge rst) delay(a_1, b_1, 700ns));
delay_s2    : assert property (@(posedge rst) delay(a_2, b_2, 700ns));

I don’t understand the issue. Elaborate with an example.
Ben systemverilog.us

*** I am not able to attach an image here which can probably explain the corner case better**

Example Corner Case:

  1. When the (posedge a) happens and if the value of b is already low(0), what it does is it looks for the next negedge of b and calculates the delay. This would cause an incorrect failure, since b is already low the property shouldn’t have failed

I have the solution if i use a clock but i am trying to find a way without using one

The following code doesn’t trigger the assertion for the actual failing case:


// minor corrected Code:
property delay (logic a,b, realtime delay);
realtime t_v[2];
disable iff (b === 0)[/b]//change from the original code
@(posedge a)(1, t_var[0] = $realtime) ##0 @(negedge b)(1, t_v[1] = $realtime) ##0(t_v[1] - t_v[0]) <= delay;
endproperty
delay_s1 : assert property (@(posedge rst) delay(a_1, b_1, 700ns));
delay_s2 : assert property (@(posedge rst) delay(a_2, b_2, 700ns));

In general what is the best practice to write an assertions for time delay between two events asynchronously?

*** I am not able to attach an image here which can probably explain the corner case better**