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

v12 are internal variables of

S . However, if they are made external variables of S ,

this would set up a simulation relation between the states of X and S , namely, a

state of X ,say .0;0;s S / would be associated only with a state of S of the form,

s S D .; ; ; ;0;0/;

i.e., the values of (v11,v12) in F are forced to take the same values as latches 4

and 5 in can have any value. All other product states would

not be allowed. For example, a product state

S , but latches 0-3 in S

will not exist since
the two copies of (v11,v12) in the product would disagree. Further, for any state
s X that

.0;0;1;1;0;1;0;1/

must agree with the state label of
s X . No other inputs can appear. This creates many input don't cares for each state
of

X is in, the u input, (v11,v12) ,to X

. We will see in Sect. 14.3 that these can be used effectively to state minimize
Xfsm by the command dcmin .
This type of forced correspondence can be introduced using the following two
steps:
(Step 1)

X

. In this example, it
would amount to adding (v11,v12) to the primary outputs of

Make latches in F additional primary outputs of S

S .

(Step 2) Make all the latches of F primary outputs of F . In the example, F would

have the additional outputs (v11,v12) .
As a result, in computing the solution X , the primary outputs of F and S are f or ced

to have the same values. This is because when taking the product of ,by

definition, two signals with the same name must have the same values. The above
two steps can be performed using BALM's command latch expose ,whichtakes
a range of latch numbers to be made into primary outputs.
Example 13.4. (continued from Example 13.3 ) We illustrate the procedure in
the

F and S

. The six latches of planet.blif are
( v7,...,v12 ). We first execute the following sequence of BALM commands:
1.read_blif planet.blif
2.latch_split 0-3
3.latch_expose 4-5 \# this makes v11 and v12 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 command latch split creates the following files: planetf.blif ,
planeta.blif , planetS.script , planetSC.script , planetL.
script , planetLC.script . The last four files are scripts to compute the
largest solutions of the general language equation and of the restricted (by
simulation) problems. In particular, the file planetS.script is a BALM script
that computes the largest solution of the restricted problem defined by setting up
a relation between the states of

example, planet.blif is S

F X and S . The solution is produced in the file

planetxs.aut .