Search code examples
system-verilogsystem-verilog-assertions

SVA Repetition Non-Consecutive Operation Qualifying Event

I have the following property:

property p;
  @(posedge clk) a |=> b[=2] ##1 c;
endproperty

It tell us that if a is asserted, then start from the next clk, b should be asserted non-consecutively two times followed by c is asserted anytime after the last b.

My question is what if c is asserted in between the first b and the second b. Should the assertion fail immediately or continue on? Some reference book says that it should fail, but I doubt it. What is the expected behavior?

Solution

  • The [= or non-consecutive repetition operator is similar to goto repetition, but the expression need not be true in the clock cycle before c is true.

    Let's say a is asserted. The implication condition is satisfied and assertion is further evaluated.

    Thereafter, b is checked two times, no matter what c is. Once b is found to be asserted for two non-consecutive clock edges, thereafter c is checked after 1-clock cycle (due to ##1).

    If c is asserted and de-asserted when b is being checked for 2 times, then that toggling is not considered. What of c is considered is after 2 assertions of b.

    Following snaps shall give a clear idea:

    Passing snap:

    Pass

    Fail snap:

    Fail

    Here, even though there was a glitch in c, the assertion didn't went through.

    Refer to A Practical Guide for SystemVerilog Assertions pdf for more details. Doulos tutorial is also a good one.