SVA: Assertion to check timing difference between a clock and a reset signal

SystemVerilog
1

Hi I’m writing an assertion to check the time difference between a clock signal and a reset. The requirement is that the delay between refclk and resetb should be greater than 90 us. This is the assertion that I have written

property clk_before_resetb(time delay);
         realtime t_var;
          disable iff(enable == 0)
        @(posedge refclk)(1, t_var = $realtime) |=>  @(posedge resetb) (($realtime - t_var) <= delay);

endproperty

The problem I face here is that it checks the assertion for every posedge of the refclk, but I need it to check only for the first posedge of the refclk toggle.

To tackle the problem of checking at every posedge, I have used $past(refclk) !== (refclk) to detect only the input edge of the refclk but the assertion still fails even though the delay is greater than 90us

property clk_before_resetb(time delay);
         realtime t_var;
          disable iff(enable == 0)
        @(posedge refclk)(1, t_var = $realtime) ##0 $past(refclk) !== (refclk)|=>  @(posedge resetb) (($realtime - t_var) <= delay);

endproperty

Are there any mistakes in the way it is coded? any solutions are much appreciated.
Thank you in advance.

2

In reply to shruti_k:


property clk_before_resetb(time delay);
         realtime t_var;
          disable iff(enable == 0)
        @(posedge refclk)(1, t_var = $realtime) |=>  @(posedge resetb) (($realtime - t_var) <= delay);
endproperty

initial begin 
   #10; // some delay if necessary 
   if(enable==0) wait(enable);
   ap_clk_before_resetb: assert property(clk_before_resetb);   
end

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Links_to_papers_books - Google Docs
Getting started with verification with SystemVerilog
https://rb.gy/f3zhh

3

In reply to ben@SystemVerilog.us:

Hi Ben ,

A slight correction , we would need to provide either a default value to input argument ’ delay ’ OR provide an actual during call to assert property :


initial begin 
   #10; // some delay if necessary 
   if(enable==0) wait(enable);
   ap_clk_before_resetb: assert property( clk_before_resetb( 10ns ) );   
end

Also thanks for sharing this interesting application wherein a concurrent assertion needs to be fired only once !!
Initial block would ensure that the property is checked only once

4

In reply to ben@SystemVerilog.us:

Hi Ben, Thank you for the reply, but I have already used the inital begin to invoke the assertion. However I do not need the enable signal anymore and just need to check the timing difference between the first posedge of the REFCLK and the RESETB.


5

In reply to shruti_k:

initial begin 
   // #10; // some delay if necessary 
   // if(enable==0) wait(enable);
   ap_clk_before_resetb: assert property( clk_before_resetb(90us) );   
end