Hardware Reference
In-Depth Information
17.2.
Recode the property
ranged_always
of Fig.
17.2
as a single recursive pro-
perty with argument local variables
low
and
high
and no other local variables. [Hint:
Manage
low
and
high
as decrementing counters instead of using the incrementing
local variable
cnt
.]
17.3.
Recode the property
ranged_until
of Fig.
17.4
as a single recursive property
with argument local variables
low
and
high
and no other local variables. [Hint:
Manage
low
and
high
as decrementing counters instead of using the incrementing
local variable
cnt
.]
17.4.
Figure
17.4
gives a recursive encoding of
p
until
[low:high] q
for general
properties
p
and
q
. Give a nonrecursive encoding under the restriction that
p
and
q
are Booleans. Try to find a nonrecursive encoding for general properties
p
and
q
.
17.5.
Write a recursive property (or a set of mutually recursive properties) to check
that properties
p0
,
p1
, and
p2
hold in cycles from the start of evaluation that are
congruent to 0, 1, and 2 modulo 3, respectively.
17.6.
Write a nonrecursive property to perform the check of property
even_odd
from Fig.
17.6
. Write a nonrecursive property to perform the check of property
even_odd_stall
from Fig.
17.7
.
17.7.
Explain why
p_fifo_data_check_recur
in Fig.
17.9
becomes illegal if
##1
is deleted from Line
8
. Assuming that
##1
is deleted from Line
8
, explain how and
why the property can be repaired by adding
nexttime
in Line
10
.[Hint:Usethe
fact that
start
and
complete
are mutually exclusive.]
17.8.
Modify the recursive encoding of the retry protocol in Fig.
17.14
so that there
is a failure if
dataValid
,
complete
,or
retry
occurs while no write transaction
is in flight. Also, check that there is never an occurrence of
complete
without
dataValid
while a write transaction is in flight.
17.9.
Make the same modifications specified in Exercise
17.8
for the nonrecursive
encoding in Fig.
17.15
.
17.10.
Let
a
and
b
be Booleans. Determine whether any of the following declara-
tions or instances violates the restrictions on recursive properties.
property
p1;
1
a |-> p2;
2
endproperty
3
property
p2;
4
p4
and
(b |-> p1);
5
endproperty
6
property
p3;
7
disable iff
(reset)
8
p4
and nexttime
(a |-> p2);
9
endproperty
10
property
p4;
11
reject_on
(bad)
12
a |=>
not
p1;
13
Search WWH ::
Custom Search