Assertions implication operator vs ##

Hi All,

property period_check(MIN,MAX);
    realtime current_time, mean_t;
    @(posedge CLK) (a==1,current_time = $time )**|=>** (1, mean_t=$time- current_time) ##0 (mean_t >= MIN && mean_t <= MAX);  
  endproperty

1)if i use "|=> " this operator check is considering a==1 ,if a==1 then only checking for consequent.
2)if use ##1 in place of |=> ,check is firing for every time WHY???

@(posedge CLK) (a==1,current_time = $time )**##1** (1, mean_t=$time- current_time) ##0 (mean_t >= MIN && mean_t <= MAX);

Thanks,
Nagendra.

Hello,

That is the main difference between |=> and ## operator in assertion.

for |=> , it will check consequent only when your antecedent will become true.
while, ## will always check whether condition is true or not.

Thanks,
Mansi

In reply to gani:

Hi,

For a ##, it checks for the expression which we write. If that is found, it immediately returns true, else it results in false.
For a |=>, it checks for the expression which we write. If that is found, it goes further, if not found it waits until it is found but does not result in an error. ALways in |=>, for the property to be true, all the expressions used in that should be true and for it to be false, the last expression should be false.