Advanced Sequences - SVA: The Power of Assertions in SystemVerilog - page 250

Fig. 11.11 previously p

property

t

clock ticks

11.2.1.1 Past Temporal Operators

In SVA, all property operators are directed to the future. For example, always p
means that from the current clock tick on the property p holds, s_eventually p
means that p happens in the current or in a future clock tick, p until q means that
p holds from now on until q happens, nexttime p means, that p holds in the next
clock tick, etc.
There exists also past temporal logic [ 34 ] in which the operators are directed or
operate on past values of signals. We illustrate such past operators in Table 11.3 .
It may be shown that past temporal operators do not add any additional expressive
power to the language. Everything that may be expressed with future and past
temporal operators may be expressed with future temporal operators only. Using
past temporal operators just makes the formulas more succinct.
The past temporal operators are not part of SVA; nevertheless, it may be of
interest to find an appropriate work-around. In the special case when the operands
are Boolean, and not arbitrary property expressions, it is natural to use sequence
method triggered as shown in Fig. 11.12 . The figure shows property definitions
that implement several past temporal operators applied to Boolean values. 6 Besides
the operators listed in Table 11.3 , the figure contains the operator first that is not
part of a past temporal logic, but is closely related to it. This operator does not have
arguments; it returns true in clock tick 0, and false in all other clock ticks.
Figure 11.12 illustrates several points that we mentioned earlier:

￿ Sequence methods can be applied to sequence instances only; therefore, we had
to create auxiliary sequences, such as seq_previously , seq_once ,etc.
￿ Sequence methods return Boolean values true (1Šb1) and false (1Šb0) .Itiscor-
rect to use Boolean negation !seq_once(!e).triggered in the implementation
of sofar instead of property negation not seq_once(!e).triggered .Thisalso
applies to the implementation of first .
￿ It is legal to apply sequence methods to a sequence with arguments, such as
seq_previously(e).triggered .
Figure 11.12 does not contain implementations of operators before and backto.
Their implementation is left to the reader as exercise (Exercises 11.15 and 11.16 )

6 For some tools, it may be more efficient to implement seq_not_first using modeling code
to set a flag after clock tick 0.