Hardware Reference
In-Depth Information
Example 22.22.
Let
D
my_always(a)
, where
a
is a Boolean. Show that for
w
a
word without any special letter
>
or
?
,
w
ˆ
iff
w
ˆ
always
a
in the unclocked
semantics.
Solution:
By definition,
w
ˆ
iff for all
k
>0,
w
ˆ
[k]
. Also by definition,
[k]
D
my_always[k](a)
By the preceding example, for all
k
>0,
my_always[k](a)
(
always
[0:k-1] a)
and nexttime
[k] 1'b1
Since
w
has no special letter,
w
ˆ
nexttime
[k] 1'b1
for all
k
>0, and so
for all 0
i<
j
w
j
;
w
i
w
ˆ
iff
ˆ
a
On the contrary,
always
a
is formally defined as
a
until
0
in Annex F of the
LRM. Since
w
has no special letter,
w
i::
6ˆ
0
for all 0
i<
j
w
j
. Therefore,
for all 0
i<
j
w
j
;
w
i
w
ˆ
always
a
iff
ˆ
a
t
Example 22.23.
Let
a
and
b
be Booleans, and let
q
be declared by
property
q(
property
p);
a |-> p;
endproperty
Determine the unclocked formal semantics of the property
D
q(my_always(q(b)))
Solution:
By definition,
w
ˆ
iff for all
k
>0,
w
ˆ
[k]
. Also by definition,
[k]
D
q[k](my_always[k](q[k](b)))
The declaration of
q
instantiates no named property, so for all
k
>0,
q[k]
D
q
.
Therefore, for all
k
>0,
[k]
q(my_always[k](q(b)))
a |-> my_always[k](a |-> b)
a |-> ((
always
[0:k-1] a |-> b)
and nexttime
[k] 1'b1)
w
ˆ
nexttime
[k] 1'b1
iff either
j
w
j
<
k
or
w
k
6D?
. Therefore,
w
ˆ
iff
either
1.
j
w
jD
0,or
2.
N
w
0
6ˆ
a
,or
3.
both
Search WWH ::
Custom Search