Assertion modelling using time delay

Problem Statement: When Signal A is de-asserted and within 700ns Signal B should be de-asserted. This property should be re-usuable.

Current Code:
property delay (logic a,logic b, time delay);
time 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));

Problem with the above code: Since i am using edge as my comparing some cases property fails incorrectly, how can I use a assert property for time delay based on level sensitivity.

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));

Problem with the above code: Since i am using edge as my comparing some cases property fails incorrectly, how can I use a assert property for time delay based on level sensitivity.

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

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**

In reply to matz25:
You’ll need to show me your model and issue.
I rewrote your assertion:

property p_delay (logic a,b, realtime delay);
        realtime t_v[2];
        @(posedge a)(1, t_v[0] = $realtime) ##0 @(negedge b)(1, t_v[1] = $realtime) ##0(t_v[1] - t_v[0]) <= delay;
    endproperty
    delay_s1    : assert property (p_delay(a, b, 750)) -> e1;
    delay_s2    : assert property (p_delay(a, b, 700ns)) -> e2;
    

Below are links to the testbench and image. Seems tot work OK.
If you have trouble putting the image on a web site (like google photo), you may email your test code and image at ben@SystemVerilog.us

http://systemverilog.us/vf/delay_test2.sv

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home


  1. SVA Alternative for Complex Assertions
    https://verificationacademy.com/news/verification-horizons-march-2018-issue
  2. SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  3. SVA in a UVM Class-based Environment
    https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment