Hardware Reference
In-Depth Information
a.
for all 0
i<
j
w
j
such that
N
w
i
ˆ
a
,
w
i
ˆ
b
, and
b.
for all 0<i <
j
w
j
,
w
i
6D?
.
t
Exercises
22.1.
Write
the
explicit
formal
semantics
for
the
operators
or
,
always
,
s_eventually
,
until
,
until_with
, and
s_until_with
.
22.2.
Prove the following semantic equivalences:
(a)
not
(p
until
q)
(
not
q)
s_until_with
(
not
p)
(b)
not
(p
s_until
q)
(
not
q)
until_with
(
not
p)
.
22.3.
Write the explicit formal semantics for the following sequences:
s[
*
n]
,
s[
*
]
,
##[
*
]s
,
r ##[
*
]s
.Here
r
and
s
are sequences, and
n
is a positive integer
number.
22.4.
Prove that
c[->1] ##0 c[->1]
c[->1]
as unclocked sequences.
22.5.
Prove that
s_nexttime
p
not nexttime not
p
as unclocked properties.
22.6.
Define
the
clock
rewriting
rules
for
the
operators
until_with
and
s_until_with
.
22.7.
For each of the event expressions below, compute the Boolean expression that
results from applying .
1.
$global_clock
iff
b.
2.
(
posedge
c
)
or
(
negedge
d
)
.
3.
(
edge
c
),
b.
4.
(
negedge
c
)
or
(
negedge
d
iff
b
)
.
22.8.
Compute clock rewrite rules for the following derived forms:
1. b
[->
n
]
(
b
[->1])[
*
n
]
.
2. b
[=
n
]
(
b
[->
n
] ##1 !
b
[
*
]
.
3.
(1,
v
1
=
h
1
,
v
2
=
h
2
)
(1,
v
1
=
h
1
) ##0 (1,
v
2
=
h
2
)
.
4. b
throughout
r
b
[
*
]
intersect
r .
5. r
1
and
r
2
((
r
1
##1 1[
*
])
intersect
r
2
)
or
(
r
1
intersect
(
r
2
##1 1[
*
]))
.
6.
s_eventually
p
not always not
p.
7.
s_nexttime
p
not nexttime not
p.
8.
if
(
b
)
p
1
else
p
2
(
b
|->
p
1
)
and
(
weak
(
b
)
or
p
2
)
.
p
.
;c/:
22.9.
Show that the following equivalences are preserved under
T
1. r
#=#
p
not
(
r
|=>
not
p
)
.
2.
reject_on
(
b
)
p
not accept_on
(
b
)
not
p.
Search WWH ::
Custom Search