Hi Ben, a quick follow up. In the accepted solution, you mentioned
"
Quote:
my_prop2: assert property( a ##[2:] b |=> ##[1:]c ##1 d);
If the consequent has an infinite range (delay or repeat), you DO NEED A GOTO OR First_match() . This is because in the consequent you also have that ORing, which means any thread is a match thread, any failed matched thread in the consequent is ignored, and the tool will look for other threads. A failure if ALL threads fail, and that will never occur because of the ##[1:]. Quote: my_prop2: assert property( a ##[2:] b |=> c[*1:$] ##1 d);
That thread CAN fail (e.g., if the c sequence is 111110XXXX
"
On that front can I say the following (Please note: I slightly modified the antecedent):
my_prop2: assert property( a ##2 b |=> ##[1:$]c ##1 d);
This property can Pass but never Fail
my_prop2: assert property( a ##2 b |=> c[*1:$] ##1 d);
This property can Fail but never Pass
Also you mentioned this rule of thumb when the ##[1:$] delay is on the antecedent
“SVA requires that each of the threads of that antecedent with a range or a repeat statement, must be tested with its appropriate consequent” → And for the assertion to pass nonvacously should all these antecedent threads pass or if just any 1 thread passes can we say the assertion to be a nonvacous pass
Similarly is there any rule of thumb (and also the condition for it to be a nonvacous pass) if the ##[1:$]delay is on the consequent, like this:
property p3;
$rose(a) |=> b ##[1:$] c;
endproperty
Thanks in advance