Hardware Reference
In-Depth Information
>
and
?
. The letter
>
satisfies every Boolean expression, even
false
, and the letter
?
does not satisfy any Boolean expression, not even
true
. In other words, for any
Boolean e,
>ˆ
e and
?6ˆ
e. These letters are mathematical devices useful only for
defining the formal semantics; there are no corresponding SystemVerilog constructs
to express them directly.
Example 22.4.
Let s denote the sequence
##1 a[
*
2]
. s is tightly satisfied on the
trace
w
1
D:
aa
>
, but it is not tightly satisfied on the traces
w
2
D:
a
:
a
>
and
w
3
D?
aa.
Note that
w
1
D:
a
ˆ
true
,as
true
is satisfied by every letter except
?
.Also,
w
1
D
a
ˆ
a.And
w
1
D>ˆ
a since
>
satisfies every Boolean expression.
Therefore,
w
1
j
s.
w
2
6j
s since
w
2
D:
a
6ˆ
a.The
>
at time 2 does not help match the sequence.
At time 1, we already have the evidence that the sequence s cannot be matched
regardless the trace content at future time moments.
w
3
6j
s since
w
3
D?6ˆ
true
:
?
does not satisfy any Boolean, not even
true
. The sequence started with unary
##1
. The important point is that this does
not simply mean to skip the first letter. Rather, the first letter must satisfy
true
.
t
Example 22.5.
Let s denote the sequence
a ##1 0
. Sequence s is tightly satisfied
on the trace
w
D
a
>
, i.e.,
w
j
s, since
w
0
D
a
ˆ
a and
w
1
D>ˆ
0. The latter
holds because
>
satisfies every Boolean expression, even 0 (or,
false
). Note that the
sequence s cannot be tightly satisfied on any trace that does not contain
>
since no
other letter satisfies
false
.
t
Example 22.6.
The property
a
until
b
is satisfied on the trace a
^:
b
>:
a
^
:
b:::. Indeed, at time 0
a
is true, and at time 1 all Boolean expressions are satisfied.
t
Example 22.7.
The property
always
a
holds on the trace
w
D
a
>:
a::: because
always
a
is a shortcut for
a
until
0
and 0 (or
false
) is satisfied by
>
(see
Example
22.6
), even though
a
does not hold in time 2.
t
22.3.3
Weak Sequential Property
Now that we have defined the extension of the alphabet, we are ready to define the
formal semantics of weak sequences:
w
j
weak
(
s
)
iff for every i
0
w
0;i
!
>
ˆ
strong
(
s
)
:
Informally, this definition means that no finite prefix of the trace can be evidence
that the sequence cannot match. As in the case of a strong sequential property the
sequence must not admit an empty match.
Search WWH ::
Custom Search