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