Vacuous success for unbounded window in SystemVerilog Assertions

Today I’d like to unleash few of the unsung features SystemVerilog assertions. As we all know the power of assertions for quickly targeting using vivid types of properties and sequences. Apart from formal verification, even in a SV/UVM based randomized verification, it is always preferable to guard all the generic blocks like arbiters, FIFOs and other custom logic by assertions. This helps in safe guarding design for any corner cases which may involve significant debug cycle.

But one feature of assertions that all of us stumble upon is vacuous passing feature. The implication (|-> or |=>) provides a capability of vacuous passing of assertions. The left hand side of the implication is called the “antecedent” and the right hand side is called the “consequent.” The antecedent is the gating condition. If the antecedent succeeds, then the consequent is evaluated. If the antecedent does not succeed, then the property is assumed to succeed by default. This is called a “vacuous success.” While implication avoids unnecessary error messages, it can produce vacuous successes.

This implies that is an assertion is triggered by satisfying antecedent condition and if the consequent condition never gets satisfied (probably due to use of ‘eventuality’ operator), then the assertion never fails. Consider the following scenario:

We have an arbiter where grant can be asserted after N number of cycles of assertion of request. To verify that we get a grant for each of request, we would have something like following property:

property check();

    @(posedge clk)

    req |-> ##[0:$] gnt;

  endproperty

But here, if the request is asserted and we never get a grant from our arbiter, then this assertion will pass vacuously at the end of sim. Even there could be a testbench timeout which can tell us that something went wrong. Debugging a reason of testbench timeout can be tedious and counter intuitive many times. But if we somehow make this assertion fail during vacuous pass, then it would help greatly in saving debug cycle.

SystemVerilog LRM provides a “strong” operator to notify the assertion failure. As per IEEE 1800-2017, Section 16.12.1:

strong(sequence_expr) evaluates to true if, and only if, there is a nonempty match of the sequence_expr.

It implies that we could exploit the following assertion to match it exactly and eliminate vacuous passes at the end of test. Here, if request is asserted, then we are waiting for at least one nonempty match for grant. The assertion will fail if we see a request and never see a grant.

property check();

    @(posedge clk)

    req |-> strong(##[0:$] gnt);

  endproperty

Since only one match of a sequence_expr is needed for strong(sequence_expr) to hold, a property of the form strong(sequence_expr) evaluates to true if, and only if, the property strong(first_match(sequence_expr)) evaluates to true.

Another way to disable vacuous pass is using system command $assertvacuousoff as described in “Assertion control system tasks” in LRM section 20.12. This works similar to $assertcontrol but at a specifically to disable the vacuous passing.

Note that by default Synopsys VCS does not enable liveliness operators for compilation. We need to add “-assert svaext” to enable these operators.

There exists other operators like s_eventually, eventually etc, which can also be good to use. Refer to the below pages for more information on liveliness checking using assertions.

  1. The power of SVA in SystemVerilog.
  2. Doulos liveliness check properties.
  3. SVA FV tutorial.

Hope that this post helps you in easing out the debug cycles… Happy Diwali..!!

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

%d bloggers like this: