Hardware Reference
In-Depth Information
p1 and p2 .If expr is true and p1 is a vacuous success, the overall property is a
vacuous success; similarly, when expr is false, p2 determines the result. If the else
clause is missing then the evaluation is nonvacuous if and only if expr is true and
the evaluation of p1 is nonvacuous. When expr is false or when p1 is a vacuous
success, the evaluation of the overall property is a vacuous success.
Most simulation and formal verification tools report vacuous successes when the
top-level property operator is one of the cases listed above. Other more complex
forms where nested property operators are involved become computationally costly
and more importantly, seldom provide results of practical importance. Nonetheless,
the subject of vacuity has been a topic of research, so the interested reader may wish
to consult [ 13 , 24 , 47 ], for instance.
An alternative way to define nonvacuous execution of an assertion that is
suitable for simulation is to define it recursively for each operator. This is how the
SystemVerilog LRM defines nonvacuity. The rules first define nonvacuous attempt
evaluation for weak and strong sequences, and then for all property operators in
terms of the evaluation of their operands.
Exercises
10.1. Rewrite Example 10.7 using a chain of if - else property operators. How
could you verify that the two forms are equivalent?
10.2.
Which properties are valid (i.e., always true)? Explain.
(a) (( s_eventually p1) and ( s_eventually p2)) iff
s_eventually (p1 and p2)
(b) (( s_eventually p1) or ( s_eventually p2)) iff
s_eventually (p1 or p2)
(c) (( always p1) implies ( always p2)) iff
always (p1 implies p2)
(d) 1'b1 until 1'b0
(e) 1'b1 s_until 1'b0
10.3.
Write a property never_p that states that its argument property p is never
true.
10.4. Write a property next_ev_p( logic b, property p) that evaluates to true
if and only if its argument p holds at the next occurrence of the Boolean expression
b . If there are not enough clock ticks for b to evaluate to true, then the property
should fail.
10.5. Write a property next_ev_a_p( logic b, int m, n, property p) that
generalizes the property from Exercise 10.4 in such a way that p must hold in
the range [m:n] of occurrences of b after the start of evaluation of next_ev_a_p .
The occurrences of b need not be consecutive. For example, if the range is [2:4] ,
Search WWH ::




Custom Search