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

i o

F

v u

X

Fig. 13.2 signals correspond

to v0,...,v6 ,the v signals correspond to v7,v8,v9,v10 (latches of the

Topology for latch splitting. In the example planet.blif the i

X component

planeta.blif ), the u signals correspond to v11,v12 (exposed latches of the

F component

planetf.blif ), the

signals correspond to v13.6,...,v13.24 .The u signals v11,v12
are exposed both in the context planetf.blif and in the specification planet.blif

o

Files planetf.blif and planeta.blif derived by latch split are
copies of planet.blif , except in planetf.blif the latches ( v7,...,v10 )
have been removed and replaced by input variables v which are named
( v7,...,v10 ). In planeta.blif the latches ( v11,v12 ) have been removed
and replaced by inputs named ( v11,v12 ). In addition, all outputs

are removed
from planeta.blif , i.e., its only output signals are ( v7,v8,v9,v10 ).
This procedure sets up the topology shown in Fig. 13.2 .
Recall that planeta.blif is a particular solution contained in

o

X (except

that it does not have logic that produces the outputs ). Thus the latches of

planet.blif have been split into the first four latches that are part of

o

A and

the remaining two that are part of F . The third command, latch expose 4-5 ,

makes those latches of , additional primary

outputs. The fourth command writes the exposed network into a new file, named
planet.mv . This file will replace planet.blif as the specification. The last
three commands expose the latches of

S , which correspond to latches of F

as required by Step 2).
Before running the script file planetS.script , it should be edited to reflect
that

F

is now called planet.mv . Initially planetS.script looks like:
\# Language solving script (partitioned) generated by MVSIS
\# for latch splitting of sequential network ''planet.blif"
on Tue Jun 22 13:45:35 2010
\# Command line was: ''latch_split 0-3".

S

echo ''Solving the language equation ... "
solve_fsm_equ planetf.blif planet.blif v0,v1,v2,v3,v4,v5,
v6,v11,v12 v7,v8,v9,v10 planetxs.aut
print_stats_aut planetxs.aut
We replace the input files, planetf.blif and planet.blif , of procedure
solve fsm equ by planetf.mv and planet.mv , since these are the new files