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

Example 5.10. Reset rst should eventually be deactivated.

Solution:

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

t

Checking s_eventually Property. The s_eventually property differs signifi-
cantly from all other properties described in this chapter. 5 Consider, for instance,
assertion a1 from Example 5.10 . Suppose that we simulated the DUT for 10,000
clock ticks and rst remained high all the time. Does it mean that assertion a1 is
wrong? No, it does not, since it might pass if we simulate few more clock cycles.
The failure of this assertion can only be observed on an infinite trace in which rst
is always high. Such assertions are called liveness assertions, and they are studied in
Chap. 21 . Generally speaking, liveness assertions cannot be falsified in simulation,
but only in FV. However, we can say something about property s_eventually
even observing its behavior in simulation: It looks suspicious if the condition of
s_eventually does not happen during simulation. For instance, when executing
any test from the testbench, it is reasonable to expect that in Example 5.10 a zero
value of rst will be observed. In the case when the condition of s_eventually has
never been observed, a simulation tool usually issues a warning message at the end
of simulation. 6

Example 5.11. What does s_eventually always p mean?
Solution: According to the definition of s_eventually this property means that
there exists some clock tick where always p is true. This is equivalent to the
statement that p is true from some clock tick on.
Discussion: Strictly speaking, this property can neither fail nor pass in simulation.
As mentioned earlier, a simulation tool may issue a warning message (or failure) at
the end of simulation if in the last clock cycle a Boolean p is false. t

Efficiency Tip. Checking property s_eventually always p in simulation may be
costly, especially if it is not in the scope of an initial procedure.

5 Here, for convenience, we use the terms “property” and “assertion” interchangeably in the context
of failure or success.
6 As we explain in Chap. 10 ,since s_eventually is a strong operator, at the end of simulation
when there are no more clock ticks and rst was high all the time, the simulator may declare
failure of the property.