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

Notice that the solution to the restricted problem (e.g., planetxs.aut )
must be contained in the solution to the general language problem (e.g.,
planetxl.aut ). This can be verified by using the command contain
in BALM. The containment may be strict or not, according to each specific
case.

Problems

13.1. By using BALM, perform the sequence of experiments explained in the
text on the example planet.blif . Be sure to understand the rationale of each
command line included in each script:

(a) Execute the following sequence of BALM commands that solves the restricted
problem F X sim S and generates the scripts planetS.script ,

planetSC.script , planetL.script , planetC.script :

1.read_blif planet.blif
2.latch_split 0-3
3.latch_expose 4-5 \# this makes v4 and v5 outputs
of planet.mv
4.write_blif_mv planet.mv
5.read_blif planetf.blif
6.latch_expose
7.write_blif_mv planetf.mv
8.source planetS.script
The result is in the file planetxs.aut .
(b) Execute the script planetSC.script to verify that the product of the
solution planetxs.aut and of the context planetf.aut is contained in
the specification planets.aut . Is the containment strict ?
Suppose that we modify the script planetSC.script by adding
v11,v12 in the last two calls to the support command. Is the containment
strict ? Explain.
(c) Execute the script planetL.script to solve the general language equation
F X S . The result is in the file planetxl.aut .

(d) Execute the script planetLC.script to verify that the product of the
solution planetxl.aut and of the context planetf.aut is contained in
the specification planets.aut . Is the containment strict ?
(e) Check whether the restricted solution planetxs.aut is strictly contained
in the general solution planetxl.aut by using the command contain in
BALM; run contain with the option -e to obtain, if any, a trace produced by
planetxl.aut but not by planetxs.aut .
13.2. Consider the sequential circuit lion9.blif whose description in the blif
language is shown in Problem 11.1.