Advanced Properties - SVA: The Power of Assertions in SystemVerilog - page 231

10.6 Vacuous Evaluation

When an assertion fails, it provides good information about the cause of the failure,
often near its source in the design code. However, what happens if no assertion fails?
Does that mean that the design is correct relative to the set of assertions used? In the
chapter on coverage (Chap. 18 ), we can see that assertion success is not a guarantee;
we still must make sure that the tests cover as much of the functionality of the design
as possible.
Many typical assertions involve one of the following conditional operators:
￿ suffix implications |-> , |=>
￿ Boolean implication ->
￿ if - else operator, or
￿ implication implies
Consider the simple Boolean property x->y where x and y are some Boolean
expressions. The interpretation of this property is if x is true then y must be true .
If x is false it does not impose any claim on y : the property is true regardless
the truth of y . This success is called a vacuous success . That is, a success that
carries no weight as far as the verification of the design is concerned. In practice,
a more desirable test is the one in which variable x evaluates to true. Therefore,
if an assertion has only vacuous successes in a test, it means that either the test
never stimulates the design in such a way as to make x true, or that the design
may never have a value assignment that makes the expression true. In the former
case, we must make sure that other tests do trigger the assertion so that it does
evaluate nonvacuously. In the latter case, we must examine x and the design to see
whether the problem is a bad formulation of the expression, or something wrong in
the design that prevents the variables from achieving the expected values. Finally,
a nonvacuous success of an assertion evaluation attempt requires that the following
two conditions be met:
￿ The assertion property attempt evaluates to true, and
￿ The evaluation attempt is nonvacuous.
The evaluation attempt of any sequential property, weak or strong (Sect. 10.1 ),
is always nonvacuous since no explicit condition is stated in a sequence. It
is essentially a pattern match based on regular expressions , and the match is
unconditional.
Now we will consider conditional expressions where vacuity is of practical
significance. For properties of the form
￿ sequence_expr |-> p
￿ sequence_expr |=> p
the evaluation is nonvacuous if sequence_expr has a match and the evaluation
thread of p that results from the match evaluates nonvacuously.
For property if (expr)p1 else p2 , an evaluation attempt is nonvacuous when
expr is true and p1 evaluates nonvacuously, or when expr is false and p2 evaluates
nonvacuously. It follows that vacuity is determined by evaluation of the properties