Outline
•
•
•
•
•
•
•
•
Composition, Conformance
Topologies
Proof of solution
Node flexibilities
Examples
Node minimization
Windowing
C-progressive
Composition
• Synchronous
• Asynchronous (parallel)
• Mapping Asynchronous to Synchronous
Composition (synthronous or asynchronous) – involves two steps
1. Make the two machines have the same input alphabet (support)
2. Perform the product
Synchronous (changing the support)
1. Projection – Given a language L over the alphabet X  Y
projection is defined as L  X  {{ Xi } | {( Xi  Yi )}  L }
2. Lifting – given a language L over the alphabet X, lifting
to the alphabet X  Y is defined as L  Y  {{( Xi  )} | { Xi }  L }
Asynchronous (changing the support)
1. Restriction – Given a language L over the alphabet X  Y ,
the restriction to X is defined as L  X  {{ p X ( i )} | { i }  L }
  i if  i  X 
where
p X ( i )  


otherw
ise


2. Expansion – given a language L over X, lifting to the
alphabet X  Y is defined as
L  Y  {{ i x i  i } | { x i }  L   i ,  i  Y }
*
Mapping Parallel into Synchronous
Suppose F is a FSM on inputs i,v and outputs u and S is an
FSM on inputs i and outputs o.
u
i
F
v
X
o
i
S
The semantics are that when an input comes into a
module, it takes an unspecified amount of time for the
module to produce an output. This will be modeled with a
non-deterministic self-loop labeled with 
o
Transitions of F (as an FSM) are one of the forms
(s i/u s’) or (s v/u s’).
For S, its transitions are of the type (q i/o q’). For each, we
convert into automata by creating new intermediate states
between inputs and outputs. Thus a transition (s i/u s’) becomes
two transitions (s i s’’) (s’’ u s’).
i/u
s
s’
Similarly for the others. For S a
transition of the type (q i/o q’)
becomes (q i q’’) (q’’ o q’).
s’’
i
s
q’’
u
i
s’
q
o
q’
We want to lift up the language of F to include o and arbitrary
delays so that iuvu becomes for example:
i oo  u  o  v  o u o  o
And S to include u and v and arbitrary delays, so that the two
languages can contain similar strings. io becomes for example
i uvu  vvvu  uu  o
In particular, they both can become the same thing:
i oo  u  o  v  o u o  o
i u  v  u  o
i u  v  u  o
i uvu  vvvu  uu  o
The common symbols act to synchronization
This is done on the automaton F by the following:
i1/u1
v1/u2
becomes
 ,o
 ,o
 ,o
 ,o
 ,o
Note the
alphabet is
 ivuo
i1
u1
v1
u2
Similarly for S:
i1/o1
becomes  , u , v
 ,u,v
i1
 ,u,v
o1
 ,u,v
i1
Note that all states
alphabet is   i  v  u  o
are deterministic since the
With these conversions, we can do synchronous composition
and get the equivalent expanded result of parallel composition S F
Thus we need to implement only one type of compositional
method – synchronous, and simply have a mapping of each
machine into its extended machine to compose in parallel.
Finally, we can take the synchronous solution and map it back
into an FSM.
Conformance
Simulation Relation ( ) Let F1 and F2
be two automata over the same alphabet 
F2 simulates F1 ( F1 F2 ) if there exists a simulation relation
S  S 1  S 2 such that


 s1 s 2  S [( s1  s )   s ' ( s 2  s 2 )  ( s1 s 2 )  S ]
'
1
'
'
'
2
Note that F2 simulates F1 implies that L ( F1 )  L ( F2 )
but these are not equivalent notions. If may be easier to
find a simulation relation than to prove language containment.
Language Containment (

)
To show that F1  F2
(i.e. L ( F1 )  L ( F2 ) ) we typically show that F1 F2  
This requires complementing F2 which may be hard if
F2 is non-deterministic (subset construction). So
simulation may be easier to check.
Use of a simulation relation instead of language
containment can allow avoidance of computing S in the
construction of F S . Note that if S is deterministic or
small, then there is no motivation to avoid computing S so
using language containment is fine.
Language Equality (
 )
L ( F1 )  L ( F2 )
Proposition: If two FSMs, F1 and F2, and F2 is deterministic,
then
( L ( F1 )  L ( F2 ))  ( L ( F1 )  L ( F2 ))
Hence, if we are solving F X  S and S is a deterministic FSM
then X  F S is the MSG.
If S is ND, then what is MSG?
Comment: Clearly, we need F  S in order for there to be a
solution of F X  S . This requires that supp(S)  supp(F),
since otherwise there is a variable v in F but not in S. Then S  v
would be too large.
Topologies
F
I1
U2
I2
X
O1
most
U1
general
O2
F
I1
U2
X
I1
I1
two-way
U1
cascade
O2
F
one-way I1
cascade
X
U2
F
X
U1
X
two-way
U1
cascade
O2
one-way
cascade
U1
O2
F
O2
O1
F
I1
U2
U1
rectification
X
F
U2
I2
Engineering
Change
U1
X
O2
Controller
F
U2
I2
X
U1=O
1
Communicating the internal state
F
I1
U2
I2
O1
U1
X
F
I1
U2
O2
I2
latch_expose
U1
X
O1
cs
O2
Hiding only the outputs
I
O
F
V
U
X
Theorem: X  ( F ( S ) U V )  I U V If
O is a deterministic function of
i,v,cs, the second complementation
is easy (no subset construction).
Thus the only variables that X
does not see are the O variables.
In the construction, for the most
general solution,
X  ( F ( S ) U V )  I U V
F ( S ) U V is deterministic. The
only variables eliminated before
complementation are O. The
only way it could become ND is
if ivuo on a pair of arcs have the
same values of ivu, but different
o’s. Thus if o is a deterministic
function of i,v, o = f (i,v,cs), this
could not happen.
Hiding the outputs only
i’u’v’o1
iuvo2
The only way it
could become
non-deterministic
after hiding o is if
i’u’v’ = iuv. But
then o1 = o2 which
means that the
product machine
was ND.
Solving a language equation
Solve A X
C
where
 { , } and
 { , , }
In particular, find the largest solution X (most general solution).
Theorem A: Let A and C be languages over alphabets I  U
and I  O respectively. For the equation, A  X  C
the most general solution is X  ( A O C U ) U O
Theorem B: Let A and C be languages over alphabets I  U
and I  O respectively. For the equation, A X  C
the most general solution is X  ( A O C U ) U  O
Proof: We prove Theorem A. Let   (U  O ) * . Then A    C
means that
  ( A O    I )  I  O  C
  ( A O    I  C  U )  I  O
  A O    I  C  U
I
  ( A O    I  C  U )  U  O
A
U
X
  (  I ) U  O  ( A O  C U ) U  O
O
    ( A O  C  U )  U  O
   ( A O  C  U )  U  O
   AC
Thus A  C is the largest solution of
The proof of Theorem B is similar.
A X  C
Computing the CF for a node global step
yi
X
Z
R( X , yi , Z )
R( X , yi )  Z [ R( X , yi , Z )  R
spec
( X , Z )]
Computing CF - local step
Yi
X
Yij
yi
yi
Z
M ( X , Yi )
CF (Yi , yi )  X [ M ( X , Yi )  R( X , yi )]
CF (Yi , yi )   X [ M ( X , Yi )  Z [ R( X , yi , Z )  R
spec
( X , Z )]]
CF
yi
Yi
yi
X
Z
M ( X , Yi )
M ( X , Yi )
Yi
yi
CF (Yi , yi )   X [ M ( X , Yi )  Z [ R( X , yi , Z )  R
 X , Z [ M ( X , Yi ) R( X , yi , Z )]R
spec
spec
(X , Z)
Note that essentially the same computation applies for multiple-output
1
k
nodes, i.e. where yi  { yi , , yi }
( X , Z )]]
FSM networks – computing
complete sequential flexibility (CSF)
i1
FSM
FSM
FSM
i2
i
Specification S (i,o)
FSM
FSM
FSM
FSM
o
spec
context
v
u
unknown
o
Context C (i,v,u,o)
Unknown X (u,v)
Problem: Given S and C , find the Most
General Solution (MGS) of
X
C  S
FSM Networks
i
The most general solution
(MGS) of
X C  S
spec
context
v
o
u
unknown
is
M G S  (C
( S )  ( i , v ,u , o ) )  ( u , v )
In general, MGS is deterministic automaton
but as an FSM it is non-deterministic (NDFSM)
Complete Sequential Flexibility (CSF)
• CSF is maximum sub-behavior in MGS
which is prefix closed and u-progressive.
– For unknown to be an FSM, it must be
progressive in its inputs
u
v
CSF
Comparison with combinational case
Sequential
i
CSF (u, v)  i ,o (C ( S )( i ,v ,u ,o ) ) ( u ,v )
spec
context
u
o
v
unknown
Combinational
CF (Yi , yi )  X , Z [ M ( X , Yi ) R( X , yi , Z )]R
R( X , yi , Z )
X
Yi
yi
unknown
(X , Z)
  X , Z [ M ( X , Yi )  R ( X , yi , Z )
R
M ( X , Yi )
spec
spec
( X , Z )]
Extending CF
FSM
I
u
O
X
Combinational
sub-block
v
Spec is IO behavior of FSM. Combinational block is treated
as unknown X with inputs u and outputs v. We derive the
CSF for X. It is different than the CF where the spec is taken
to be the combinational behavior of the FSM, i.e. with inputs
I,CS and outputs O,NS.
Also, if we extract from X a maximum combinational
subpart (combinational projection), it is also different that
CF
Algorithm
Algorithm: LanguageEquationSolving
Input: prefix-closed deterministic S(i.o) and C(i,v,u,o)
Output: most general prefix-closed,
progressive X (FSM)
begin
01
X := Complete ( S, non-accepting )
02
X := Determinize&Complement ( X )
S
03
X := Support (X, (i,v,u,o)) - raise
( S )( i ,v ,u ,o )
03
X := Product ( C, X )
(C ( S )( i ,v ,u ,o ) )
04
X := Support ( X, (u,v) ) - hide (C ( S )
)
 ( i ,v ,u ,o ) ( u ,v )
05
X := Determinize
&Complement ( X, u ) (C ( S )( i ,v ,u ,o ) )( u ,v )
06
return Prefix&Progressive (X ) Convert to FSM
end
Examples
• Games
–
–
–
–
Nim
Tic-tac-toe
Toe-tac-tic
Board
• Control
– Wolf, goat, cabbage
• Latch splitting
Example: Coin Game (NIM)
In God We
Trust
In God We
Trust
In God We
Trust
1.
2.
3.
Context describes the state of the
game and legal moves. Its input is
random moves by first player and its
output tells if the game is in a losing,
winning or continuing state.
Specification is a 3-state
automaton, playing, won, and lost.
Players alternate turns
On each turn, player can take 1-n coins from any one pile
Player who takes last coin loses
Winning strategy: Give your opponent a pile of coins
with even number of 1’s in bit columns (except at end)
Example: 6 5 3
6=110
5=101
3=011
____
222
NIM
spec.mva
.model spec
.inputs out
.outputs Acc
.mv out 3 OK notOK done
.mv CS,NS 3 a b c
.table CS ->Acc
.default 1
b0
.table out CS ->NS
OK a a
notOK a b
done a c
-bb
-cc
.latch NS CS
.reset CS
a
.end
.model game-piles
.inputs p1 d1 p2 d2
.outputs out
.mv
.mv
.mv
.mv
.mv
p1,p2,p,pt,ptt 3
d1,d2,d 7
cs0,cs1,cs2,ns0,ns1,ns2,nh,h 7
whoseturn,whoseturn1 2 1 2
out 3 OK notOK done
.latch
.reset
3
.latch
.reset
2
.latch
.reset
1
ns0 cs0
cs0
ns1 cs1
cs1
ns2 cs2
cs2
.latch whoseturn1 whoseturn
.reset whoseturn
1
#set this to 2 if Player 2 goes first.
.table whoseturn whoseturn1
.default 2
2 1
.table whoseturn d1 d2 d
1 - - =d1
2 - - =d2
.table whoseturn p1 p2 ptt
1 - - =p1
2 - - =p2
# Map move into a legal move
.table ptt cs0 cs1 cs2 pt
0 (1,2,3,4,5,6) - - 0
1 - (1,2,3,4,5,6) - 1
2 - - (1,2,3,4,5,6) 2
0 0 - - 1
1 - 0 - 2
2 - - 0 0
.table pt cs0 cs1 cs2 p
0 (1,2,3,4,5,6) - - 0
1 - (1,2,3,4,5,6) - 1
2 - - (1,2,3,4,5,6) 2
0 0 - - 1
1 - 0 - 2
2 - - 0 0
#selects the height of the pile chosen by player 1
.table p cs0 cs1 cs2 h
0 - - - =cs0
1 - - - =cs1
2 - - - =cs2
#computes h-d. If h<=d then =0
.table h d nh
.default 0
6 1 5
6 2 4
6 3 3
6 4 2
6 5 1
5 1 4
5 2 3
5 3 2
5 4 1
4 3 1
4 2 2
4 1 3
3 2 1
3 1 2
2 1 1
# The next state ns is due to the move.
.table p nh cs0 ns0
0 - - =nh
(1,2) - - =cs0
.table p nh cs1 ns1
1 - - =nh
(0,2) - - =cs1
.table p nh cs2 ns2
2 - - =nh
(0,1) - - =cs2
#"out" indicates who the winner is.
.table whoseturn ns0 ns1 ns2 out
.default OK
1 0 0 0 done
2 0 0 0 notOK
.end
Lang.script (NIM)
rl fixed.mv
stg_extract fixed.mva
echo "Synthesis ..."
determinize -ci spec.mva spec_dci.mva
support p2(3),d2(7),p1(3),d1(7),out(3) spec_dci.mva spec_dci_supp.mva
support p2(3),d2(7),p1(3),d1(7),out(3) fixed.mva fixed_supp.mva
product fixed_supp.mva spec_dci_supp.mva p.mva
support p1(3),d1(7),p2(3),d2(7) p.mva p_supp.mva
determinize -ci p_supp.mva p_dci.mva
prefix p_dci.mva p_dci_pre.mva
progressive -i 2 p_dci_pre.mva x.mva
minimize x.mva x-min.mva
prefix x-min.mva x-min.mva
echo "Verification ..."
support p2(3),d2(7),p1(3),d1(7),out(3) x.mva x_supp.mva
product x_supp.mva fixed_supp.mva prod.mva
support p2(3),d2(7),p1(3),d1(7),out(3) spec.mva spec_supp.mva
check prod.mva spec_supp.mva
mvsis 02> source lang.script
The STG with 40 states and 110 transitions is written to file "fixed.mva".
Synthesis ...
The automaton is deterministic; determinization is not performed.
Product: (40 st, 110 trans) x (3 st, 5 trans) -> (42 st, 112 trans)
The automaton is deterministic; determinization is not performed.
Warning: The automaton has been completed before state minimization.
State minimization: (22 states, 45 trans) -> (13 states, 30 trans)
Verification ...
Product: (21 st, 34 trans) x (40 st, 110 trans) -> (21 st, 34 trans)
Warning: Automaton "game-piles*spec*game-piles" is completed before checking.
The behavior of "game-piles*spec*game-piles" is contained in the behavior of "spec".
mvsis 03> psa x-min.mva
"game-piles*spec": incomplete (9 st), deterministic, non-progressive (9 st), and non-M
oore (9 st).
4 inputs (4 FSM inputs) 12 states (12 accepting) 19 trans
Inputs = { p1(3),d1(7),p2(3),d2(7) }
mvsis 03>
Example of CSF computation:
NDFSM represented as automaton
Inputs p1(3),d1(7)
Outputs p2(3),d2(7)
In God We
Trust
In God We
Trust
In God We
Trust
Tic-tac-toe
spec.mv
.model spec
.inputs m1 c1 m2 c2
.outputs out
.mv m1,m2 9
.mv out 3
.table ->out
0
2
.end
spec.mva
#
.model spec
.inputs out
.outputs Acc
.mv out 3
.mv CS,NS 3 a b c
.table CS ->Acc
.default 1
b0
.table out CS ->NS
0aa
1ab
2ac
-bb
-cc
.latch NS CS
.reset CS
a
.end
.model game-tic-tac-toe
.inputs m1 m2
.outputs out
.mv out 3
.mv m1,m2,m 9
.mv cs0,cs1,cs2,cs3,cs4,cs5,cs6,cs7,cs8 3
.mv ns0,ns1,ns2,ns3,ns4,ns5,ns6,ns7,ns8 3
.mv whoseturn,whoseturn1 2 1 2
.latch whoseturn1 whoseturn
.reset whoseturn
1
.latch ns0 cs0
.reset cs0
0
.latch ns1 cs1
.reset cs1
0
.latch ns2 cs2
.reset cs2
0
.latch ns3 cs3
.reset cs3
0
.latch ns4 cs4
.reset cs4
2
# set this to 0 if player 2 makes the second move.
.latch ns5 cs5
.reset cs5
0
.latch ns6 cs6
.reset cs6
0
.latch ns7 cs7
.reset cs7
0
.latch ns8 cs8
.reset cs8
0
.table illegal whoseturn whoseturn1
021
012
1 - =whoseturn
.table whoseturn m1 m2 m
1 - - =m1
2 - - =m2
# Player makes a illegal move if the square indicated by mt in not empty
.table m cs0 cs1 cs2 cs3 cs4 cs5 cs6 cs7 cs8 illegal
.default 1
00--------0
1-0-------0
2--0------0
3---0-----0
4----0----0
5-----0---0
6------0--0
7-------0-0
8--------00
# out records if there is a line of 2's (then out=2) or a line of 1's (then out=1)
.table whoseturn ns0 ns1 ns2 ns3 ns4 ns5 ns6 ns7 ns8 out
.default 0
2--2-2-2-- 2
2222------ 2
22--2--2-- 2
22---2---2 2
2---222--- 2
2--2--2--2 2
2-2--2--2- 2
2------222 2
1--1-1-1-- 1
1111------ 1
11--1--1-- 1
11---1---1 1
1---111--- 1
1--1--1--1 1
1-1--1--1- 1
1------111 1
# Once the game gets into a winning configuration, do not change the state.
.table cs0 cs1 cs2 cs3 cs4 cs5 cs6 cs7 cs8 done
.default 0
--2-2-2-- 1
222------ 1
2--2--2-- 1
2---2---2 1
---222--- 1
--2--2--2 1
-2--2--2- 1
------222 1
--1-1-1-- 1
111------ 1
1--1--1-- 1
1---1---1 1
---111--- 1
--1--1--1 1
-1--1--1- 1
------111 1
# If there is a winner (done=1) then the state remains unchanged.
# Otherwise, if m=i and whoseturn=1, then csi=1. Similarly, if
# m=i and whoseturn=2, then csi=2
.table illegal done cs0 m whoseturn ns0
#.default 0
0 1 - - - =cs0
00-011
00-022
0 0 - (1,2,3,4,5,6,7,8) - =cs0
1 - - - - =cs0
.table illegal done cs1 m whoseturn ns1
#.default 0
0 1 - - - =cs1
00-111
00-122
0 0 - (0,2,3,4,5,6,7,8) - =cs1
1 - - - - =cs1
.table illegal done cs2 m whoseturn ns2
#.default 0
0 1 - - - =cs2
00-211
00-222
0 0 - (0,1,3,4,5,6,7,8) - =cs2
1 - - - - =cs2
.table illegal done cs3 m whoseturn ns3
#.default 0
0 1 - - - =cs3
00-311
00-322
0 0 - (0,1,2,4,5,6,7,8) - =cs3
1 - - - - =cs3
.table illegal done cs4 m whoseturn ns4
#.default 0
0 1 - - - =cs4
00-411
00-422
0 0 - (0,1,2,3,5,6,7,8) - =cs4
1 - - - - =cs4
.table illegal done cs5 m whoseturn ns5
#.default 0
0 1 - - - =cs5
00-511
00-522
0 0 - (0,1,2,3,4,6,7,8) - =cs5
1 - - - - =cs5
.table illegal done cs6 m whoseturn ns6
#.default 0
0 1 - - - =cs6
00-611
00-622
0 0 - (0,1,2,3,4,5,7,8) - =cs6
1 - - - - =cs6
.table illegal done cs7 m whoseturn ns7
#.default 0
0 1 - - - =cs7
00-711
00-722
0 0 - (0,1,2,3,4,5,6,8) - =cs7
1 - - - - =cs7
.table illegal done cs8 m whoseturn ns8
#.default 0
0 1 - - - =cs8
00-811
00-822
0 0 - (0,1,2,3,4,5,6,7) - =cs8
1 - - - - =cs8
.end
Lang.script (tic-tac-toe)
rl fixed1.mv
latch_expose
stg_extract fixed.mva
echo "Synthesis ..."
determinize -ci spec.mva spec_dci.mva
support cs0(3),cs1(3),cs2(3),cs3(3),cs4(3),cs5(3),cs6(3),cs7(3),cs8(3),
whoseturn(2),m1(9),m2(9),out(3) spec_dci.mva spec_dci_supp.mva
support cs0(3),cs1(3),cs2(3),cs3(3),cs4(3),cs5(3),cs6(3),cs7(3),cs8(3),
whoseturn(2),m1(9),m2(9),out(3) fixed.mva fixed_supp.mva
product fixed_supp.mva spec_dci_supp.mva p.mva
support cs0(3),cs1(3),cs2(3),cs3(3),cs4(3),cs5(3),cs6(3),cs7(3),cs8(3),
whoseturn(2),m2(9) p.mva p_supp.mva
determinize -ci p_supp.mva p_dci.mva
prefix p_dci.mva p_dci_pre.mva
progressive -i 10 p_dci_pre.mva x.mva
minimize x.mva x-min.mva
prefix x.mva x-min.mva
Wolf, goat, cabbage
.model wolfe
.inputs in
.outputs out
.mv in,in1 4 empty wolfe goat cabbage
.mv csw,csg,csc,nsw,nsg,nsc 3 left right boat
.mv bank,bank1 2 left right
.mv out 3 OK notOK done
.latch stop1 stop
.reset stop
0
.latch nsw csw
.reset csw
left
.latch nsg csg
.reset csg
left
.latch nsc csc
.reset csc
left
.latch bank1 bank
.reset bank
left
.table out stop stop1
.default 0
done - 1
-11
.table stop bank bank1
.default left
0 left right
1 - =bank
out
in(boat)
.table stop bank in1 csw nsw
0 left (empty,goat,cabbage) boat left
0 left wolfe (left,boat) boat
0 right (empty,goat,cabbage) boat right
0 right wolfe (right,boat) boat
0 - (empty,goat,cabbage) (left,right) =csw
1 - - - =csw
.table stop bank in1 csg nsg
0 left (empty,wolfe,cabbage) boat left
0 left goat (left,boat) boat
0 right (empty,wolfe,cabbage) boat right
0 right goat (right,boat) boat
0 - (empty,wolfe,cabbage) (left,right) =csg
1 - - - =csg
.table stop bank in1 csc nsc
0 left (empty,goat,wolfe) boat left
0 left cabbage (left,boat) boat
0 right (empty,goat,wolfe) boat right
0 right cabbage (right,boat) boat
0 - (empty,goat,wolfe) (left,right) =csc
1 - - - =csc
.table bank nsw nsg nsc out
.default OK
right left left - notOK
left right right - notOK
right - left left notOK
left - right right notOK
right (right,boat) (right,boat) (right,boat) done
# map input (in) into any legal input
.table bank in csw csg csc in1
.default empty
right wolfe (right,boat) - - =in
left wolfe (left,boat) - - =in
right goat - (right,boat) - =in
left goat - (left,boat) - =in
right cabbage - - (right,boat) =in
left cabbage - - (left,boat) =in
.end
spec.mva
for wolf-goat-cabbage
.model spec
.inputs out
.outputs Acc
.mv out 3 OK notOK done
.mv CS,NS 3 a b c
.table CS ->Acc
.default 1
b0
.table out CS ->NS
OK a a
notOK a b
done a c
-bb
-cc
.latch NS CS
.reset CS
a
.end
lang.script
rl wolfe.mv
stg_extract fixed.mva
echo "Synthesis ..."
determinize -lci spec.mva spec_dci.mva
support in(4),out(3) spec_dci.mva
spec_dci_supp.mva
support in(4),out(3) fixed.mva fixed_supp.mva
product -l fixed_supp.mva spec_dci_supp.mva p.mva
support in(4) p.mva p_supp.mva
determinize -lci p_supp.mva p_dci.mva
prefix p_dci.mva p_dci_pre.mva
progressive -i 0 p_dci_pre.mva x.mva
minimize x.mva x-min.mva
prefix x-min.mva x-min.mva
echo "Verification ..."
support in(4),out(3) x.mva x_supp.mva
product x_supp.mva fixed_supp.mva prod.mva
support in(4),out(3) spec.mva spec_supp.mva
check prod.mva spec_supp.mva
Wolf, goat, cabbage
x.mva
Minimized
x-min.mva
Other Games
1. Toe-tac-tic (solvable)
–
–
–
Like tic-tac-toe
Except that any player can play either X or O at any
time
A player wins when he completes a line or either X’s
or O’s
2. Board game (too many states)
–
–
–
–
–
4 x 4 board
Each player has 4 pieces which initially at the top and
bottom rows of the board.
Any piece can move forward, left or right
Player wins when he moves one of his pieces to the
other side
12870 reachable states – can’t do it right now
Application - splitting FSM blif files
u
i
FSM
FSM1
v
XFSM2
o
This is just a syntactic change. Nothing has been done yet.
Latch split
i
S
o
mvsis 05> _split -h
Usage: _split [-v] <latch_list>
splits the current network S into two parts: F and X
generates the script to solve the equation F * X = S
-v : toggles verbose [default = no]
<latch_list> : the list of latches to be included in X
no spaces are allowed in the latch list
the numbers of latches are zero-based
for example: 0,3,5-7,9
mvsis 05>
o
i
cs2
cs1
S
.model s27.bench
.inputs G0 G1 G2 G3
.outputs G17
.reset G5 0
.latch G10 G5
.reset G6 0
.latch G11 G6
.reset G7 0
.latch G13 G7
.table G0 G1 G3 G5 G6 G7 G17
.default 0
11---- 1
1-0--- 1
1----1 1
---1-- 1
-1--0- 1
--0-0- 1
----01 1
.table G0 G1 G3 G5 G7 G10
.default 0
11--- 1
1-0-- 1
1--1- 1
1---1 1
.table G0 G1 G3 G5 G6 G7 G11
.default 0
0--01- 1
-010-0 1
.table G1 G2 G7 G13
.default 0
10- 1
-01 1
.end
Latch_split example
s27f (F)
s27a (X’)
.model s27.bench
.inputs G0 G1 G2 G3 G5 G6
.outputs G17
.model s27.bench
.inputs G0 G1 G2 G3 G7
.outputs G17
.latch G13 G7 0
.latch G10 G5 0
.latch G11 G6 0
.names G0 G1 G3 G5 G6 G7 G17
11---- 1
1-0--- 1
1----1 1
---1-- 1
-1--0- 1
--0-0- 1
----01 1
.names G0 G1 G3 G5 G7 G10
11--- 1
1-0-- 1
1--1- 1
1---1 1
.names G0 G1 G3 G5 G6 G7 G11
0--01- 1
-010-0 1
.names G1 G2 G7 G13
10- 1
-01 1
.end
.names G0 G1 G3 G5 G6 G7 G17
11---- 1
1-0--- 1
1----1 1
---1-- 1
-1--0- 1
--0-0- 1
----01 1
.names G0 G1 G3 G5 G7 G10
11--- 1
1-0-- 1
1--1- 1
1---1 1
.names G0 G1 G3 G5 G6 G7 G11
0--01- 1
-010-0 1
.names G1 G2 G7 G13
10- 1
-01 1
.end
# Language solving script generated by MVSIS
# for sequential network "s27.blif" on Wed Feb 18 21:35:53 2004
# Command line was: "split 0,1".
echo "Solving the language equation ... "
solve s27f.blif s27.blif G0,G1,G2,G3,G7 G5,G6 s27x.aut
psa s27x.aut
echo "Verifying the containment of the known implementation ... "
read_blif s27a.blif
latch_expose
stg_extract s27a.aut
support G0,G1,G2,G3,G7,G5,G6 s27a.aut s27a.aut
check s27a.aut s27x.aut
read_blif s27.blif
s27x.aut
s27x-dcmin.aut
s27a.blif
G0, G1, G2, G3, G7, G5, G6
inputs
outputs
FSM networks - Node Minimization
Given a NDFSM CSF, find the “smallest” FSM
Y, such that Y is well-defined and
Y  CSF
Y is called a reduction of CSF
State graph of X
It generally looks like
non-accepting
don’t care state
C-compatibility - dcmin
Two states s1 and s2 are c-compatible if their
care sets do not intersect, i.e. the care set of
one is completely contained in the don’t care
set of the other. s s states
1
2
u
u-space
Remaining
DC
Care
Care set
set
v
X (cs,u,v,ns)
Y (cs, u )  v , ns X (cs, u, v, ns)
Y (s1 , u)  Y (s2 , u)  
A simple state reduction method-dcmin
• Let X ( s, v, u, s ') be the relation for the incomplete CSF X, and
compute Y ( s, u )  v , s ' X ( s, v, u, s ')
– i.e. those states and inputs for which there exists a next state
and output (the next state can be either accepting or not).
• Order this BDD with the u variables first, and let pi ( s) be the
unique functions below the u variables pointed to.
• Two states s1 and s2 are c-compatible if and only if for all i,
pi ( s1 )  pi ( s2 )  0 i.e. they have no minterm u in common.
• So pi ( s) is a clique of states that can't be merged, i.e. are not ccompatible and must have different colors.
• Then the c-incompatibility graph is I (s, s ')   pi (s) pi (s ')
i
which has to be colored.
• Suppose Q( s, c) is the assignment of states s to colors c. The
new automaton relation for X is then
X '(c, v, u, c ')  s , s ' Q( s, c) X ( s, v, u, s ')Q( s ', c ')
Simple state reduction
Merged
states
u-space
Care
Care
Remaining set
Care set
DC
set
Note that this is a
“simple” coloring problem
in contrast to the
compatibilities problem
normally associated with
state minimization for
incompletely specified
FSMs.
In contrast, here a group
of states is “c-compatible”
iff they are pair-wise ccompatible.
Other ideas on reduction of CSF
• This problem is similar to SOP minimization when using CF to
minimize the node in the combinational network.
• Many cost functions are possible. If we try to minimize the number
of states in CSF, it is the problem of minimizing a PNDFSM –
– T. Kam et. al., DAC 1994.
• We might want to look for a good implementation directly, rather
than first minimizing the number of states.
– Similarly, for a node in the combinational circuit, looking for a small SOP,
or the minimum number of literals in FF, may be misleading.
• A specialized algorithm has been developed to check whether a
combinational solution (a single-state reduction) exists.
– The problem is reduced to SAT with as many variables as there are states +
transitions in the CSF. Solution is practical for, say, 100 states and 500
transitions.
– A similar algorithm can be developed to check whether a 2 or 3 state
solution exists
• more variables, the SAT problem is harder
Iterative language solving
The problem of computing the CSF can be iterative.
1.
2.
3.
4.
5.
6.
7.
8.
Given F and S
Split F into F1 and F2
Solve F1 * X = S.
If we can reduce X to a smaller implementation than F2, replace
F2
Solve F2 * X = S
If we can reduce X to a smaller implementation than F1, replace
F1
Set F = F1 * F2
If either F1 or F2 has changed, go to 2
FSM Windowing
FSM1
i
X
X1
FSM2
X2
FSM3
X3
X = X1 * X2 * X3
Compositionally
Progressive
spec
i
o
F
v
u
X
• X should be compositionally progressive (c-progressive) with F
– i.e. for every product state cs of X * F, the next state ns and output o should be
defined for all i.
• Roland Jiang has proposed a way to use this to additionally trim the solution X
during the subset construction. But he is not 100% sure it is right.
• Nina and Tiziano have another method for trimming and have proved that the
largest c-progressive solution can contain well-defined FSM sub-behaviors that
are not c-progressive.
• Roland has demonstrated that the above paper is wrong.
• Being c-progressive does not necessarily imply no combinational loops
• To hear a more detailed discussion, attend MVSIS weekly meeting Friday, 111pm in DOP center library (fishbowl)
• There might be a connection here with omega-automata.
Future developments
• Objective is to push to the limit, the size of application
that can be done
– Keep multi-level MV structure, given in MVSIS, as long as
possible (lecture on this later)
– Use SAT in subset construction
• The bottleneck looks to be extracting good subbehavior of CSF (reduction)
– A sub-graph of the CSF usually not good enough
– “Simplified” (dcmin) state minimization of CSF may be good
first step?
• Try for a good sub-behavior more directly without
constructing CSF
• Try hierarchy and windowing applied to FSM network
Descargar

Document