Hardware Reference
In-Depth Information
a
A
b
−
0
/
00
A
−
1
/
00
−
1
/
10
−/
00
−/
10
C
−
0
/
01
−
0
/
11
B
B
−
1
/
11
−
0
/
10
−
1
/
01
D
Fig. 13.4
Example for Problem
13.3
.(
a
) Fixed component
M
A
(variables
IV=U
1
U
2
/
;(
b
)
Specification
M
C
(variables
I=U
1
U
2
)
S
A
S
C
is defined to be a simulation relation
Definition 13.3.1.
A relation
M
A
D .S
A
;I V;U O;T
A
;r
A
/
from the fixed machine
to the specification
M
C
D .S
C
;I O;T
C
;r
C
/
if and only if:
.r
A
;r
C
/ 2
1.
,and
s
A
i
o
!
M
A
s
v
=
u
0
A
0
A
2.
.s
A
;s
C
/ 2 )
8i 9
v
8
u
8o 8s
s
C
.
i=o
!
M
C
s
0
C
0
C
0
A
;s
0
C
/ 2
)9s
^ .s
0
C
Notice that, since by logic the quantification
9s
can be brought in front and by
0
A
0
A
hypothesis of determinism
8s
can be replaced by
9s
(there is a unique next state),
the second clause in Definition
13.3.1
can be replaced by the following one:
i
o
!
M
A
s
v
=
u
0
A
9s
0
C
0
A
.s
A
;s
C
/ 2 )
8i 9
v
8
u
8o 9s
s
A
s
C
.
i=o
!
M
C
s
0
C
0
A
;s
0
C
/ 2
)
^ .s
(a) Consider the following algorithm proposed to compute the maximal simulation
relation
max
:
M
C
.
b. Repeat until convergence the greatest fixed point computation:
a. Start
as the collection of all pairs of states from
M
A
and
i
v
=
u
o
!
M
A
s
0
A
0
A
R
iC1
.s
A
;s
C
/ D R
iC1
.s
A
;s
C
/ ^
8i 9
v
8
u
8o 8s
s
A
.
i=o
!
M
C
s
0
C
0
C
0
A
;s
0
C
/
)9s
s
C
^ R
i
.s
c. If
.r
A
;r
C
/ 62 R
iC1
there is no solution, otherwise
R
iC1
.s
A
;s
C
/
is the
maximal simulation relation
max
.
Search WWH ::
Custom Search