Hardware Reference
In-Depth Information
Table 6.2 Initial trace
fragment from Example 6.2
Clock tick a b
0
1
1
1
0
0
2
0
1
3
1
1
Boolean sequence a&&b matches trace fragment 0:0 if its initial point is 0, and
trace fragment 3:3 when its initial point is 3. For initial points 1 and 2 there are no
sequence matches.
t
6.2
Sequential Property
Although a sequence itself cannot be true or false, it is possible to associate with a
sequence a sequential property (or sequence property ) in the following way: 1
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 (the notion of empty
match is explained below in this section).
This definition is applicable only to sequential properties in the context of
assertions or assumptions. In the context of cover statements, the definition of
sequential property is different, as explained in Chap. 18 . Except for Chap. 18 we
will assume that in all examples sequential properties are written in the context of
assertions or assumptions.
Although it is not easy to understand the full meaning and the rationale of the
definition of a sequential property at this point, because we have not yet described
the SVA constructs in which all nuances of this definition come into play, we need
this definition now to build properties from sequences. We will explain some of its
aspects here, while the other aspects will become clear to the reader only later.
Consider the most important special case of this definition: if a sequence has
at least one match, then the corresponding sequential property is true. The entire
definition is broader since it allows in some cases sequential properties to be true
even if their sequences do not have any match. However, if there is some number
L>0such that all matches of sequence s have a length L then if s does not
have any match then the sequential property s is false. Indeed, in this case the fact
that sequence s does not have any match on a trace fragment of length L witnesses
its inability to have any match. We will call such sequences bounded sequences .
It is easy to see that all Boolean sequences are bounded, as all their matches are one
clock cycle long.
1 Actually, there is more than one way to associate a property with a sequence, as explained in
Chaps. 10 and 22 . The definition provided in this section relates to the weak sequential property.
 
Search WWH ::




Custom Search