Hardware Reference
In-Depth Information
and V (from the first fault domain). But it also contains FSMs which are not products
of the Context with any FSM. These are called “infeasible” machines in the sense
that they cannot be decomposed into the product of the Context and another FSM.
Problems
16.1. Solve the FSM equation M A ˘ M X M C ,where M A is the context FSM
shown in Fig. 16.2 a, and M C is the specification FSM in Fig. 16.2 c. Define the
related automata A and C and carry on the following automata computations:
1. C
2. C \ .IO/ ?
3. .C \ .I O/ ? / *U[V
4. A \ . C \ .IO/ ? / *U[V
5. .A \ . C
\ .IO/ ? / *U[V / +U[V
6. .A \ .C
\ .IO/ ? / *U[V / +U[V
7. .A \ .C
\ .IO/ ? / *U[V / +U[V
\ .U V / ?
16.2. Solve the FSM equation M A ˘ M X Š M C ,where M A is the context FSM
shown in Fig. 16.2 a, and M C is the specification FSM in Fig. 16.2 c. Given the
solution of the companion FSM equation M A ˘M X
M C
obtained in Problem 16.1 ,
how does one solve this FSM equation?
16.3. Consider the parallel composition in Fig. 16.1 ,where M A is the context FSM
shown in Fig. 16.2 a, and M C is the specification FSM in Fig. 16.2 c.
Given the implementations Imp1 and Imp2 of the FSM Emb , shown respectively
in Fig. 16.4 a, b, for each implementation find external test suites to detect whether
it is faulty, based on the information provided by the largest solution of the related
FSM equation.
b
a
u 1 / v 2
u 1 / v 2
u 1 / v 1
u 1 / v 1
u 2 / v 1
u 2 / v 2
u 2 / v 2
u 2 / v 1
c
u 1 / v 2
u 2 / v 2
Fig. 16.4
( a ) FSM Imp1 ;( b ) FSM Imp2 ;( c ) FSM Imp2
 
Search WWH ::




Custom Search