Difference between implication (->) and ##0 in SVA

First thing that you have to check is syntax of single implication operator that is a |-> b.

In SystemVerilog assertion, there are two expressions.
a ##0 b
a |-> b

Actually, it looks like a similar in expressions. First of this expression is checking a is asserted(1) and after 0 clock cycle b is asserted(1) or not. Second expression is checking b is (on)asserted when a is asserted(1) then on same posedge b is asserted(1) or not.

Now, practically when verification engineers wrote this kind of assertions they take care of following things.
a ##0 b: In this expression, if a is not asserted then it shows failure.
When a is asserted(1) and on same time stamp b is not asserted then also shows failure.

a |-> b: In this expression, if a is asserted and b is not asserted then it will show a failure.
If a is not asserted then it is not going to check whether b is asserted or not. This behaviour is different than a ##0 b.

If you apply different inputs data then you can see that expression a ##0 b will give you more failure than a |-> b. Reason for same is already explained above.

One more thing to note down is "The implication construct can be used only with property definitions. It cannot be used in sequences."

Source: stack overflow