Hardware Reference
In-Depth Information
22.10.
The following facts about the SVA formal semantics can be proved:
If
w
ˆ
p and
w
0
results from
w
by changing zero or more letters to
>
, then
w
0
ˆ
p.
a.
If
w
ˆ
p and
w
0
results from
w
by changing zero or more letters away from
?
,
then
w
0
ˆ
p.
b.
Use these facts to prove the following:
If 0
i<j<
j
w
j
and
w
0;j
1
!
ˆ
p, then
w
0;i
1
!
1.
>
>
ˆ
p.
If 0
i<j<
j
w
j
and
w
0;i
1
!
ˆ
p, then
w
0;j
1
!
2.
?
?
ˆ
p.
How do these implications relate to the formal semantics of resets?
22.11.
Let
a
,
b
, and
c
be Booleans. Determine the dependency digraph for the
following declarations.
property
p1;
1
case
(a)
2
1'b0: p2;
3
1'b1: p3;
4
endcase
5
endproperty
6
property
p2;
7
p4
or
(b
and nexttime
p1);
8
endproperty
9
property
p3;
10
p4
and nexttime
(a |-> p2);
11
endproperty
12
property
p4;
13
a |=> c;
14
endproperty
15
Which properties are recursive and which are non-recursive?
22.12.
Let
my_until
be as declared in Fig.
17.3
.Let
a
and
b
be Booleans. Show
that for
k
>0,
my_until[k](a,b)
is equivalent to
weak
( (a[
*
0:k-1] ##1 b)
or
(a[
*
k] ##1 1) )
Show that
my_until(a,b)
is equivalent to
weak
(a[
*
] ##1 b)
22.13.
Let
a
be a Boolean. Show that for any word
w
, including special letters
>
and
?
,
w
ˆ
my_always(a)
implies
w
ˆ
a
until
0
. Show that the converse can
fail if
>
is a letter in
w
. (cf. Example
22.22
.)
Search WWH ::
Custom Search