Hardware Reference
In-Depth Information
Iteration:
The sequence s
[+]
(also written as
s[
*
1:$]
) is tightly satisfied on the
word
w
iff it is possible to break
w
into one or more words so that each of them
tightly satisfies s:
w
j
s
[+]
iff there exist words
w
1
;
w
2
;:::;
w
j
.j
1/ so that
w
D
w
1
w
2
:::
w
j
and for every i so that 0<i
j
w
i
j
s.
First Match:
The first match
first_match
.s/ of the sequence s is tightly satisfied
on the word
w
iff s is tightly satisfied on some prefix x of
w
then the suffix y of
w
must be empty:
w
j
first_match
(
s
)
iff
w
j
s and there exist x, y so that
w
D
xy and
N
x
j
s
then y
D
".
N
x is explained in
22.3.2
).
22.3
Formal Semantics: Sequences and Properties
In Sect.
22.1
, we defined how to build up the semantics of properties recursively,
starting from Boolean properties. However, from Chap.
6
we know that properties
are built on top of sequences and that the sequential property serves as the basic
building block for other properties. In this section, we define the formal semantics
of the properties built on top of sequences.
22.3.1
Strong Sequential Property
w
ˆ
strong
.s/ iff there exists i
0 so that
w
0;i
j
s.
Note the condition i
0—tight satisfaction on the empty word does not make the
strong sequential property hold. In fact, the LRM [
8
] states that a sequential property
admitting empty match is illegal.
Example 22.3.
strong
(
e
[
*
])
is illegal according to the LRM [
8
] because eŒ
admits empty match. Even so, consider applying the rule above for its semantics
on the trace
w
D:
e
!
where at each position e evaluates to 0. The only match
of eŒ
on a prefix of
w
is empty, but the rule above requires nonempty match for
property satisfaction.
t
22.3.2
Extension of Alphabet
Before we proceed to the definition of the formal semantics of weak sequential
properties, we need to revisit the alphabet definition. In Sect.
21.2.2
, we defined the
model alphabet as the set of all variable valuations: ˙
D
2
V
. For the purposes of
the weak sequence definition discussed in Sect.
22.3.3
, and of the reset definition
discussed in Chap.
13
, we need to extend the alphabet ˙ with two special letters:
Search WWH ::
Custom Search