Basic Sequences - SVA: The Power of Assertions in SystemVerilog - page 118

“Of course, it will. There was no truck crossing it until now, and the bridge hasn't
collapsed yet”?
There exist different definitions of vacuity [ 13 , 36 ], the LRM provides a
minimal set of rules that the tools are expected to check. We are not going to
provide the entire list of vacuous scenarios in this topic. The main source of the
vacuous execution for assertions is the case we described: when the antecedent is
false. Chapter 10 provides further details on vacuity.

Example 6.25. Property ok |-> !err passes vacuously iff ok is false. But the
equivalent property err |-> !ok passes vacuously iff err is false. Therefore, the
assertion vacuity depends on the exact style in which it is written. t

6.5 Consecutive Repetition

We will begin this section with a motivational example.

Example 6.26. Write a sequence stating that a transmission phase lasting three
consecutive cycles is followed by a receiving phase lasting two consecutive cycles.
The transmission phase is represented by signal trn , and the receiving phase is
represented by signal rcv
Solution: trn ##1 trn ##1 trn ##1 rcv ##1 rcv .
Discussion: This sequence defines a trace fragment of five clock cycles such that in
the first three cycles trn is true, and in the last two cycles rcv is true. For example,
trn may also be true in the fourth or the fifth cycle of the fragment, and also in any
clock cycle outside this trace fragment.

t

The sequence from Example 6.26 looks verbose, but the situation it describes
is typical. In SVA, there is a special operator to denote a consecutive repetition of
a sequence sn times, where n is a nonnegative elaboration time integral constant:
s[ * n] (see Fig. 6.9 ).
Example 6.27. Using the shortcut notation for the consecutive repetition, the
sequence from Example 6.26 may be rewritten as trn[ * 3] ##1 rcv[ * 2] .

t

Example 6.28. The assertion from Example 5.18 “Reset rst must be asserted
during first two cycles” may be more elegantly expressed using sequences:

t

initial a1: assert property (@( posedge clk) rst[ * 2]);