The way how threading works in assertions

In reply to yourcheers:
Does that mean, from the below code property p0 is same as having 5 different independent properties p1,p2,p3,p4,p5.
NO. However, it means the property ORing of all these properties.


$rose(a) ##[1:5] b |-> ##3 c; // is equivalent to
// Using your properties above
ap_1to5: assert property(@(posedge clk) p0 AND p1 AND p2 AND p3 AND p5); 
// In one property, it really means 
($rose(a) ##1 b) OR 
($rose(a) ##2 b) OR  
($rose(a) ##3 b) OR  
($rose(a) ##4 b) OR  
($rose(a) ##5 b)  |-> ##3 c; 

I stringly encourage you to read my paper
Understanding the SVA Engine,
https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2
That paper will clarify many of your misunderstandings with assertions and properties.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. 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
  1. 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/