I am trying to check a time from reset de-assertion to first clock cycle using assertion

[kuldeep_b]

property reset_to_clk_start_delay(CLK,RST) ;
time reset_deassert_time ;
@(posedge top_clk_491)
disable iff(ccr_disable)
($fell(RST),reset_deassert_time = $time) |-> (##[1:100] $rose(CLK),$display(“time = %t”,$time)) ##0(($time - reset_deassert_time) > worst_reset_delay_path);
endproperty

assert_reset_to_clk_start_delay_clk_61: assert property (reset_to_clk_start_delay(clk_61,rst_61));

the top_clk491 is high free running clock of 491Mhz and 61 specifies low 61Mhz clock. i am expecting the time from reset deassertion to first clock edge time should be greater than worst reset delay path.
But when i simulate even if the failure should happen at the first edge (my timing is such that it should fail) the assertion goes beyond first edge and validates at the second edge, to pass.
Somehow the ##[1:100] is propagating and taking in comparison and the $rose(CLK) as one.
What i want is to measure and check time at first edge. Please suggest…

[ben2]

In reply to kuldeep_b:

($fell(RST),reset_deassert_time = $time) |-> (##[1:100] $rose(CLK),$display("time = %t",$time)) ##0(($time - reset_deassert_time) > worst_reset_delay_path);
// is of the form 
expr1 |-> ##[1:100] expr2 ##0 expr3; 

// That is equivalent to 
expr1 |-> ##1 expr2 ##0 expr3 or  // T1
          ##2 expr2 ##0 expr3 or  // T2
          ... 
          ##100 expr2 ##0 expr3;  // T3
// Thus, if in T1  ##1 expr2==1 and expr3==0, that thread is ignored because of the "or" 
// Thus, if in T2  ##1 expr2==1 and expr3==0, that thread is ignored because of the "or"
// ... 
// The FIX
expr1 |-> first_match(##[1:100] expr2) ##0 expr3; 
// For your property  
property reset_to_clk_start_delay(CLK,RST) ;
   realtime reset_deassert_time ; // <<<<<<<<< Use realtime 
   @(posedge top_clk_491)
   disable iff(ccr_disable)
  ($fell(RST),reset_deassert_time = $realtime) |-> // <<<<<< Use $realtime 
    first_match( (##[1:100] $rose(CLK),$display("time = %t",$time)) ) ##0
               (($time - reset_deassert_time) > worst_reset_delay_path);
endproperty
 

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

• SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
• A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
• Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
• Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
• Component Design by Example ", 2001 ISBN 0-9705394-0-1
• VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
• VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115

---

1. SVA Alternative for Complex Assertions
   Verification Horizons - March 2018 Issue | Verification Academy
2. SVA: Package for dynamic and range delays and repeats | Verification Academy
3. SVA in a UVM Class-based Environment
   SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy

[kuldeep_b]

In reply to ben@SystemVerilog.us:
thanks Ben for clarification. my understanding for ##[1:100] was little flawed in terms of expr1 and expr2.
Thanks again…