Overlapping and Non-Overlapping Implication code

Hi,
My specification is as follows -
Two cycles after start** , the signal** transfer must be high.
Which one defines the specification correctly ?

//RULE_1
property rule_1;
@(posedge clk)
$rose(start) |-> ##2 $rose(transfer);
endproperty

//RULE_2
property rule_2;
@(posedge clk)
$rose(start) |=> ##2 $rose(transfer);
endproperty

In RULE_2 I use a Non-Overlapping Implication operator.
(a |=> b) equivalent to ( a |-> ##1 b)
So the simulator will check for $rose(transfer) , three cycles after start.
Is my understanding correct?

Thanks.

Yes, you’re right!

This:


property rule_2;
@(posedge clk)
$rose(start) |=> ##2 $rose(transfer);
endproperty

Is equal to this:


property rule_2;
@(posedge clk)
$rose(start) |-> ##3 $rose(transfer);
endproperty

In reply to lucaskoelho:

Thanks lucaskoelho.