Basic Properties - SVA: The Power of Assertions in SystemVerilog - page 99

Example 5.12. Reset rst remains low starting from some moment.

Solution:

initial
a2: assert property (@( posedge clk) s_eventually always !rst);

Discussion: Note the difference between assertion a2 and assertion a1 from
Example 5.10 . Assertion a2 checks that rst at some moment becomes and remains
low, whereas assertion a1 only checks that rst becomes low.
Exercise 5.5 discusses the meaning of a2 when it is a stand-alone assertion. As
we mentioned above, the stand-alone version of this assertion may be inefficient in
simulation. t

Example 5.13. What does property always s_eventually p mean?
Solution: According to the definition of always this property means that property
s_eventually p holds in every clock tick i . This is equivalent to saying that for
every clock tick i there is a clock tick j i where p is true. So,
always s_eventually p
holds if p is true infinitely many times, in other words, p is true infinitely often.
Discussion: This property can only be verified on infinite traces in formal verifica-
tion because simulation traces are finite. t

Efficiency Tip. Checking property always s_eventually p may be costly in
simulation.

Example 5.14. A pending request req should be eventually granted ( gnt is asser-
ted). This includes the case when the request is granted immediately.
More specifically, it is given that when the request becomes active it remains
active until it is granted.

Solution: Consider an arbitrary clock tick i . The assertion should be satisfied in
both of the following cases:
1. req is never asserted in all clock ticks i .
2. req is asserted for the first time ( i ) in some clock tick j i , and gnt is asserted
for the first time ( j ) in some clock tick k j . In this case, req will also be
pending until clock tick k.

Both cases imply that the attempt of the property s_eventually req -> gnt
starting in the clock tick i is satisfied, and assertion

a1: assert property (@( posedge clk) s_eventually req -> gnt);
covers the desired behavior of the pending request. Note that a1 only checks the
behavior of the grant in response to req . It does not check that a grant is not issued
without a request. It also does not check that request, once issued, persists until
granted.