Overlapping assertion scenario

SystemVerilog
,
1

I have a assertion like following
assert property ( @(posedge clk) $rose(in_sig) |-> ##[5:10] $rose(out_sig)

I have in_sig pulse in 2nd clock cycle and 4th cycle (two pulses)
The out_sig pulse is seen in 8th clock cycle and 10th clock cycle (two pulses)

However, at 8th clock cycle, assertion fails because
tool, at 8th clock cycle, checks the distance between 2nd pulse of in_sig and first pulse of out_sig (difference is 4 clock cycles)

This is a overlapping case

How to avoid this problem. Is there any switch.

2

In reply to prasad_holla:
See Assertion on req and gnt signals | Verification Academy
The concept is basic:

  1. Tag every assertion attempt with a tag number, and then increment that tag.
  2. Each active assertion checks in the consequent that the tag being serviced now is the
    same as its own tag before proceeding to the rest of the consequent.
  3. Every serviced assertion, whether it passes or fails, increments the serviced tag to
    allow another pending assertion to continue.
    Ben Cohen
    http://www.systemverilog.us/ ben@systemverilog.us
    ** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
    …
  4. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  5. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  6. Papers:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/

3

In reply to ben@SystemVerilog.us:
What I provided above is the solution for each attempt to be resolved independently from other attempts, thus a single pass does not conclude all active attempts.
However, your example and conclusions don’t seem correct.


$rose(in_sig) |-> ##[5:10] $rose(out_sig)
/* I have in_sig pulse in 2nd clock cycle and 4th cycle (two pulses)
The out_sig pulse is seen in 8th clock cycle and 10th clock cycle (two pulses)

However, at 8th clock cycle, assertion fails because */
// [Ben] I don't see the failure by analysis, see timing below.
/* tool, at 8th clock cycle, checks the distance between 2nd pulse of in_sig and first pulse of out_sig (difference is 4 clock cycles)*/ /* 
tick     0  1  2  3  4  5  6  7  8  9  10 11 12 
in_sig         1     1
out_sig                          1      1
Attempt1       ^  +--+--+--+--|==|==|==|==|==|  Pass at cycle 8  
##[5:10]                      <-------------->
Attempt2             ^  +--+--+--+--|==|==|==|==|==|   Pass at cycle 10
##[5:10]                            <-------------->    */