CODEWITHSUNDEEP
system-verilogsystem-verilog-assertions
AldoT
AldoT

Reputation: 943

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?

Upvotes: 0

Views: 1750

Answers (2)

Convergent
Convergent

Reputation: 130

In short, yes it will pass. Regardless of where c is asserted, after two "b"s are observed, it will wait until c==1. So, if c was 1 from the beginning and never goes to zero, it will pass too.

One more point to make is when this assertion will actually fail. It will pass when c is asserted, but if not, it will keep running until the end of the test! You will see the failure only at the end of simulation.

Upvotes: 0

sharvil111
sharvil111

Reputation: 4381

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.

Upvotes: 3

Related Questions