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

Example 5.4. Reset rst should be low in clock clk tick 9.

Solution:

initial a1: assert property (@( posedge clk) nexttime [9] !rst);

Discussion: This property does not say anything about the behavior of rst in clock
ticks 0-8. t

Finite and Infinite Traces. The definition of property nexttime is not as trivial
as it may seem. When we require a property to be true in the next clock tick we
implicitly assume that the clock ticks at least one more time. This observation holds
when clocks tick infinitely many times, and hence traces are infinite. Infinite traces
allow us to ignore this important question in the definition of property operators,
namely, what happens if the clock stops ticking in the middle of evaluation. Note
that this question is important even for Boolean properties: How can we define the
truth of a Boolean property on the empty trace? We do consider property behavior
on finite traces in Chaps. 10 and 22 , but in this chapter we ignore it because we wish
to concentrate on the main behavior of property operators.

Efficiency Tip. nexttime with a big factor is inefficient both in simulation and in
FV. Try to keep the factor small, especially in complex assertions. In simulation, it
is recommended not to exceed several hundred for simple argument properties, and
in FV not to exceed a couple of tens. The common rule is the smaller the better.

5.3 Always Property

Property always p is true in clock tick i iff p is true in all clock ticks j i . It follows
(see Sect. 5.1 ) that property always p is true iff property p is true in every clock
tick, as shown in Fig. 5.3 .
Property always p defines a series of “instances” of property p starting at
clock ticks 0; 1; : : :. We say that an always property defines a series of evaluation
attempts of the underlying property. For the always property to be true, all of the
underlying attempts must evaluate to true.

p p p p p p

p

Fig. 5.3 always property clock ticks