Computation of Flexibility in Sequential Networks - The Unknown Component Problem: Theory and Applications - page 168

o

u

i

M A M B

v

( M A ￿M B ) i×u×o = M KN

A

u

v M B

Fig. 10.7 Topology for Wang-Brayton's construction applied to latch-splitting example

This is converted into the Kim-Newborn topology shown in Fig. 10.7 .
We use the example s386.blif from the iscas89 benchmark suite and do
latch splitting on this. The inputs i are v6,v5,v4,v3,v2,v1,v0 .The u vector,
v9,v8,v7 and the v vector, v12,v11,v10 , are produced by the latch split
command. The BALM commands (with comments) executed are

W&B-K&N script - example s386.blif
read_blif s386.blif
latch_split 0-2
\# produces files s386f.blif and s386a.blif
latch_expose
\# exposes all latch outputs v7 - v12 of s386.blif
extract_aut MA.aut
\# since s386.blif is already the product MA x MB, this is
\# MA x MB and will become the Kim--Newborn abstract driving
\# machine MAˆRN for MB (it is the composition of s386a.blif
\# and s386f.blif which is just s386.blif)
support v6,v5,v4,v3,v2,v1,v0,v9,v8,v7,v12,v11,v10 MA.aut
MAs.aut
\# restricts support to i,u,v
complete MAs.aut MAsc.aut
determinize MAsc.aut MAd.aut
minimize MAd.aut MAd_min.aut
\# this is the abstract driving machine MAˆKN of Kim--Newborn
\# for MB
read_blif s386a.blif
\# this is MB
latch_expose
\# we need to expose the v variables which are the latch
\# outputs of MB
\# forces the v variables of MA x MB to agree with the v
\# variables of MB