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