SVA: Use of implication (|=>) vs sequence?

Question

SystemVerilog Assertion properties can be built with implication operators |=> and sequences ##1

For example :

property P1;
  @(posedge clk)
    A ##1 B |=> C ##1 D;
endproperty

Above we have used A ##1 B as an enabling sequence (antecedent) and C ##1 D as the fulfilling sequence (consequent).

I do not see why it could not be rewritten as :

property P2;
  @(posedge clk)
    A ##1 B ##1 C ##1 D;
endproperty

When and why would you choose implication |=> over a sequence ##1 ?

Answer 1

The above properties are the same for the sequence passing, however the failure conditions do not match.

If they are all 1's then A ##1 B ##1 C ##1 D; and A ##1 B |=> C ##1 D; are true.

If we have A as 1 then the rest 0's:

A ##1 B ##1 C ##1 D; fails and A ##1 B |=> C ##1 D; would pass.

The latter is not considered a failure due to the conditions of the enabling sequence not being met.