Hardware Reference
In-Depth Information
a
a
b
i 1 /o 1
i 1 v 1 /u 2 o 1
i 1 v 2 /u 1 o 2
i 2 v 1 /u 1 o 2
i 2 v 2 /u 2 o 2
a
2
i 1 /o 2
i 2 /o 2
i 2 /o 2
c
d
u 1 /v 1
u 2 /v 2
u 1 /v 2
i 1 /o 1
s
p
as
ap
i 1 /o 2
u 1 /v 1
u 2 /v 2
i 2 /o 2
u 2 /v 1
i 2 /o 2
e
f
u 1 /v 1
u 2 /v 2
i 1 /o 1
s
p
as
ap
u 1 /v 1
i 2 /o 2
u 2 /v 1
i 2 /o 2
g
h
u 2 /v 2
u 1 /v 2
i 1 /o 1
s
p
as
ap
i 1 /o 2
u 1 /v 1
i 2 /o 2
u 2 /v 1
i 2 /o 2
Fig. 3.6 Illustration of Example 3.18 .( a ) Context FSM M A ;( b ) Specification FSM M C ;
( c ) Largest Solution FSM M S ;( d ) M A
M S
Š
M C ;( e )FSMM S1 ,
reduction
of M S ;
( f ) M A M S1 M C ;( g ) FSM M S2 , reduction of M S ;( h ) M A M S2 Š M C
3.3.1.1
Complexity of the Algorithm
Consider the equation A X C ,whereA and C are FSM l anguages. We know that
the largest unconstrained solution is given by S D A C . Given the rectification
topology in Fig. 1.1d with M B as the unknown M X , the solution has in the worst-
case 2 j S A j :2 j S C j states, where S A are the states of FA A and S C are the states of
FA C . The exponent 2 j S C j appears w hen C is non-deterministic, to account for
the determinization needed to compute C ; otherwise if C is deterministic, in place
of 2 j S C j we have j S C j , because complementation becomes a linear operation. The
product j S A j :2 j S C j is due to the product of automata A and C . Then to complete the
computation of the operator we must project the product on the internal signals U
and V ; as a result we may get again a non-deterministic automaton, and therefore
Search WWH ::




Custom Search