@ben thanks for the response, apart from the above 5 cases, are there any other cases where this property is true?
Does that mean, from the below code property p0 is same as having 5 different independent properties p1,p2,p3,p4,p5.
property p0;
$rose(a) ##[1:5] b |-> ##3 c;
endproperty
property p1;
$rose(a) ##[1] b |-> ##3 c;
endproperty
property p2;
$rose(a) ##[2] b |-> ##3 c;
endproperty
property p3;
$rose(a) ##[3] b |-> ##3 c;
endproperty
property p4;
$rose(a) ##[4] b |-> ##3 c;
endproperty
property p5;
$rose(a) ##[5] b |-> ##3 c;
endproperty
I am just confused from the explanation below where there is an “and” between the properties, I was thinking it as a property “and” operator between various threads. “($rose(a) ##[1] b |-> ##3 c)” and “($rose(a) ##[2] b |-> ##3 c)”
SVA requires that each of the threads of that antecedent with a range or a repeat statement, must be tested with its appropriate consequent. Thus,
$rose(a) ##[1:5] b |-> ##3 c; // is equivalent to
($rose(a) ##[1] b) or ($rose(a) ##[2] b) or …($rose(a) ##[5] b) |-> ##3 c;
// This ORing in the antecedent creates multiple threads, something like:
($rose(a) ##[1] b |-> ##3 c) and // separate thread
($rose(a) ##[2] b |-> ##3 c) and // separate thread
…
($rose(a) ##[5] b |-> ##3 c); // last thread