SystemVerilog Assertions

Question

For the following property assertion:

property COMPLEX_SEQ;
    @(negedge CLK) disable iff (X)
        (C ##1 B[*1:3] ##1 A) |=> (J[*4] ##1 K);
endproperty

1. And the following sequences:
   a. C;B;A;J;J;J;J;K
   b. C;B;B;B

Why don't they fail? The left hand expression is not true, so why does it proceed and check the right hand expression (a)?

2. And the following sequence:
   C;B;BA;BA;A;J;J;J;J;K;

Why does it fail? both expressions are true

Thanks!

Answer 1

With implication, if the left hand side (antecedent) is false, the assertion passes vacuously. It's only when the antecedent is true do you attempt to evaluate the right side (consequent). The assertions fails only when the antecedent is true and the consequent is false.

You have to be very carful using ranges with implications. They basically create a series of OR sequence operations. In 2., there is match as soon as B is true for one cycle and A is true the next. It fails because J is not true on the next cycle.

You might want to read this thread for more information.