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

The sequential property defined by sequence s is true in clock tick i iff there is no finite
trace fragment i W j witnessing inability of sequence s with the initial point i to have a
match. Sequence s should not admit an empty match.
When we introduced this definition, we were familiar only with bounded
sequences—sequences all of whose matches happen within a finite time interval.
For bounded sequences, the definition of sequential property can be simplified: the
sequential property defined by a bounded sequence is true iff the sequence has at
least one match (Sect. 6.2 ). 5 Using the sequence operators described in this chapter,
sequences built on top of infinite delay or repetition ranges are unbounded , i.e., they
can have arbitrarily long matches. For such sequences, the definition of sequential
property cannot be simplified any more.
In our example, sequence ##[ * ] gnt is unbounded. Any finite trace fragment
does not witness the inability of this sequence to match. Indeed, the fact that gnt
did not assume high value during first 1,000 clock ticks starting from the sequence
initial point, does not prevent gnt to assume high value in the future. Therefore,
sequential property ##[ * ] gnt is true, regardless of the actual values of gnt , and
assertions a2_wrong and a3_wrong pass even if req is never granted. The correct
solution was provided in Example 6.23 :
a4: assert property (@( posedge clk) req |=> s_eventually gnt);
An alternative way to encode this assertion is discussed in Chap. 11 .
Although a sequential property of the form ##[ * ]s is meaningless, since it is a
tautology, the sequence ##[ * ]s itself is not. We saw in Example 6.46 that operator
##[ * ] modified the meaning of the implication. Namely, assertion
initial
a_always: assert property (@( posedge clk) ##[ * ] s |-> p);
checks implication s |-> p in every clock cycle, whereas assertion
initial
a_once: assert property (@( posedge clk) s |-> p);
checks this implication only once.
The definition of sequential property should be clear at this point for both
bounded and unbounded sequences. However, its rationale has not been explained
yet. Even worse, the behavior or assertions a2_wrong and a3_wrong is nonintuitive
according to this definition. Nevertheless, this definition has many advantages that
will be explained only in Chaps. 10 and 22 . In this chapter, we will only provide one
additional example, further clarifying the definition of sequential property.
We mentioned in Example 6.34 that a sequential property of the form
a[ * ] ##1 b is equivalent to property a until b . This equivalence is intuitive,
and it is conditioned by the definition of the sequential property. Indeed, property
a[ * ] ##1 b fails iff there is a finite fragment of the trace witnessing that sequence
a[ * ] ##1 b cannot have a match. This only happens if before the first occurrence of
5 As follows from the definition, all sequence matches should be non-empty.