Why can't we use followed by instead of implication operator in SVA as the default operator?

In reply to pkumar16:

You need to understand that an assertion attempts to satisfy a property every clock cycle.

If you just had

assert property (@(posedge clk) A ##1 B;)

This says on every clock edge A must be true AND B must be true the next cycle. So effectively A must be true EVERY clock cycle, and B must be true EVERY. clock cycle except for the first.

By using an implication, you are saying that it’s OK that A is true or false any clock cycle, but on the cases when it’s true, B must be true the next clock cycle.

assert property (@(posedge clk) A |=> B;)

It’s possible that A was never true, and you would need to write another kind of assertion to make sure that it does, if that is your requirement. When you collect coverage, you can also detect that the consequent never passed.