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

Example 5.3. Assume that initially the reset rst is active, and check that initially
the value of ready is low.
Solution:

initial begin
m1: assume property (@( posedge clk) rst);
a1: assert property (@( posedge clk) !ready);
end

t

The behavior manifested by a Boolean property alone when placed in an
initial procedure is useful because only one property evaluation attempt is
executed. Placing such an assertion elsewhere would lead to unconditional evalu-
ation of the Boolean at every assertion clock tick.

5.2 Nexttime Property

Property nexttime p , as its name suggests, is true in clock tick i iff property p is
true in clock tick i C 1. For a trace, according to the general definition (Sect. 5.1 ),
property nexttime p is true iff property p is true in clock tick 1, as shown in
Fig. 5.2 .
If p is a Boolean expression e , nexttime e means that e is true in the clock
tick 1.

Multiple nexttime Operators. What happens if we apply the nexttime ope-
rator twice: nexttime nexttime p ? According to the definition, it means that
nexttime p holds in clock tick 1, which is equivalent to the statement that p
holds in clock tick 2. Similarly, nexttime nexttime nexttime p means that p
holds in clock tick 3, and so on. Since having a big chain of nexttime operators
makes the property unreadable, SVA provides a shortcut nexttime [n] , where n
is an elaboration time constant. For example, nexttime [3] p is a shortcut for
nexttime nexttime nexttime p . It is also legal to specify nexttime [0] p ,
which is roughly equivalent to just p in the case of singly clocked assertions. 3

Its

semantics in multiply clocked properties is described in Chap. 12 .
nexttime is seldom used on its own. The following example illustrates such
usage.

p

Fig. 5.2 nexttime
property clock ticks

3 This is further discussed in Sect. 10.5 .