For the following property assertion:

property COMPLEX_SEQ;
    @(negedge CLK) disable iff (X)
        (C ##1 B[*1:3] ##1 A) |=> (J[*4] ##1 K);
  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)?

  1. And the following sequence:

Why does it fail? both expressions are true



1 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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.