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.