Language Solving Using Simulation Relations - The Unknown Component Problem: Theory and Applications - page 212

I O

M A ( fixed )

I O

MC

V U

M X ( unknown )

Fig. 13.3 Rectification topology for Problem 13.3

(a) Execute the following sequence of BALM commands that solves the re-
stricted problem

F X sim S

and generates the scripts lion9S.script ,
lion9SC.script , lion9L.script , lion9tC.script :

1.read_blif lion9.blif
2.latch_split 0-1
3.latch_expose 2-3 \# this makes v4 and v5 outputs
of lion9.mv
4.write_blif_mv lion9.mv
5.read_blif lion9f.blif
6.latch_expose
7.write_blif_mv lion9f.mv
8.source lion9S.script

The result is in the file lion9xs.aut .
(b) Execute the script lion9SC.script to verify that the product of the
solution lion9xs.aut and of the context lion9f.aut is contained in the
specification lion9s.aut .
(c) Execute the script lion9L.script to solve the general language equation
F X S

. The result is in the file lion9xl.aut .
(d) Execute the script lion9LC.script to verify that the product of the
solution lion9xl.aut and of the context lion9f.aut is contained in the
specification lion9s.aut .
(e) Check whether the restricted solution lion9xs.aut is strictly contained
in the general solution lion9xl.aut by using the command contain in
BALM; run contain with the option -e to obtain, if any, a trace produced by
lion9xl.aut but not by lion9xs.aut .

M A and M C are deter-

13.3. For the interconnection topology in Fig. 13.3 ,where

M A is Moore, consider the problem to solve M A M X M C ,

ministic machines and

M X is Moore too.
In Sect. 13.1 , we showed how to compute a simulation relation for the controller's
topology; consider the following proposal to extend the computation of a simulation
relation to the rectification topology of Fig. 13.3 (proposed by Satrajit Chatterjee,
class project report at UC Berkeley).

requiring that