Transcript flex

Sequential Flexibility
Overview
• Computing flexibilities in combinational logic
•
networks
FSM networks
– Computing sequential flexibilities
– Contrasting combinational and sequential flexibility
computations
– FSM minimization using register splitting
• Examples
Minimizing a Node –
Computing the Flexibility at a Node
Combinational
Logic Network
Definition. A flexibility at a node is a relation (between
the node’s inputs and output) such that any welldefined sub-relation used at the node leads to a
network that conforms to the external specification.
Definition. The complete flexibility (CF) is the maximum
flexibility possible at a node.
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
 X , Z [M ( X , Yi )  R( X , yi , Z )  R
spec
( X , Z )]]
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 spec ( X , Z )]]
 X , Z [ M ( X , Yi ) R( X , yi , Z )]R spec ( X , Z )
Note that essentially the same computation applies for multiple-output
1
k
nodes, i.e. where yi  { yi , , yi }
FSM networks
• Network of finite state machines (FSMs)
i1
FSM
Sequential
FSM
FSM
i2
Problem: Compute
the Complete
FSM
FSM
FSM
FSM
o
Flexibility of a
node
Complete Sequential Flexibility
CSF is the maximum set of FSM behaviors
(represented by a pseudo-non-deterministic
FSM), such that implementing any sub-behavior
and replacing the sub-network by the new
implemented part does not violate the
specification of the total network.
FSMs and Automata
If the distinction between inputs
and outputs is taken away (i/o
becomes io), then an FSM
becomes an automaton.
It has the following properties
as an automaton
– All states are accepting
– It is incomplete
• can make it complete by
adding one nonaccepting state
– Its language is
• prefix closed
• i -progressive
0/0
0
0
0/0
0
0
Automaton
FSM
1/1
1
1
1/0
1
0
1/0
1
0
0/0
0
0
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
is
spec
context
v
o
u
unknown
MGS  (C ( S )( i ,v ,u ,o ) )( u ,v )
In general, MGS is deterministic automaton
but as an FSM it is non-deterministic (NDFSM)
Languages.
A Language is set of finite length strings on the symbol set
 i.e. a subset of *
(a b c a c d f g g g)
At this point, we don’t care how the language is
generated or represented. So initially the comments
apply to all kinds of languages
A symbol can be made up of a vector of
variable values, e.g. 1a3de0 or 010010.
These are examples of a single symbol.
Languages can be manipulated as follows:
• Union L1  L2  { |   L1 or   L2 }
 Intersection L1  L2  { |   L1    L2 }
 Complement L  { |  *    L}
Language over cross-product of alphabets
• A language over X  Y where X and Y are symbol sets consists
of finite strings of pairs
(1 , 1 ), ( 2 ,  2 ),
, ( k ,  k )
Such that  i  X and i  Y
Projection and Lifting
Given a Language L over the alphabet X  Y
projection is defined as –
L X  {{ Xi }|{( Xi Yi )}  L}
Given a Language L over the alphabet X lifting
to the alphabet X  Y is defined as LY  {{( Xi )}|{ Xi }  L}
where - stands for any symbol in Y
Classes of Languages
 A language is prefix closed if
 * ,  ,[   L    L]
 A language over   I  O is I-progressive if
 * , i  I , o  O [  L   io  L]
Composition of Languages
Given disjoint alphabets I,U,O and languages L1 over I  U
and L2 over U  O their synchronous composition is
L1  L2  [( L1 )O  ( L2 ) I ] I O
.
Solving a language equation
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
I
A
U
X
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
A X  C
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
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
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: 5 3 6
6=110
5=101
3=011
____
222
Example of CSF computation:
NDFSM represented as automaton
The CSF is a non-deterministic FSM
5 inputs, 5 outputs, 21 states, 34 transitions
Inputs p1_0 p1_1 d1_0 d1_1 d1_2 Outputs p2_0 p2_1 d2_0 d2_1 d2_2
In God We
Trust
In God We
Trust
In God We
Trust
Computational Procedure
Computing the transition
relation of CSF
1. Complement S
Specification: S (i,o)
Context:
C (i,v,u,o)
(these have been
converted into automata)
S
2. Raise S to variables of C
3. Compose S with C
( S )( i ,v ,u ,o )
4. Hide variables not in X
(C ( S )( i ,v ,u ,o ) )( u ,v )
5. Complement result
(C ( S )( i ,v ,u ,o ) )( u ,v )
(C ( S )( i ,v ,u ,o ) )
Finite Automata
A finite automaton (FA) is F  ( S , ,  , r , Q)
where S is a set of states,  is an input alphabet,
 ( s,  ) : S    2 S
is a transition relation, r is the initial state, and Q  S
is the set of accepting states.
An input sequence
w  ( w1...wn )  *
leads from r to s’ if there exists a sequence of states,
(r  s0 s1... sn  s ')
such that si1   ( si , wi ) for all i = 0, ... ,n-1.
w is in the language of F ( w  L ( F ) )
if and only if w leads from r to s '  Q
i.e.  (r , w)  Q   where  (r , w)
denotes the set of states that can be reached from r
under the input sequence w.
Theorem: A languages is regular if and only if it is the
language of a finite automaton
Theorem: The set of all languages for deterministic
FA is the same as for non-deterministic FA.
(this can be shown by using the so-called subset
construction.)
Operations on FA.
projection ( F X ): convert F over X  V
into F’ over X by replacing each edge (xv s s’) by the
edge (x s s’)
lifting (FV ): convert F over X into F’ over X  V

by replacing each edge (x s s’) by ( x V s s ') where V
stands for any v  V
.
Operations on FA.
Product
Given FAs F1 and F2 both over  , the product is
F  F1F2  ( S1  S2 , ,  ,(r1r2 ), Q1  Q2 )
where  ( s1s2 , )  1 ( s1 , )   ( s2 , )
Complementation
If F is deterministic, thenF  ( S , ,  , r , Q  S  Q)
.
If F is non-deterministic, the only known way for
complementation is to determinize it first. This is
done by the sub-set construction.
Composition
Synchronous Composition. Given two automata F1
and F2 over alphabets I  U
and U  O
their synchronous composition is
F1  F2  ( F1 )O ( F2 )I
i.e. the product of the two automata when they are
made to have the same alphabet.
Subset Construction
Given NFA
F  ( S , ,  , r , Q) we create a DFA F’ with the same language as F:
F '  (2S , ,  ',{r}, Q ')
S
where Q '  {s '  2 | qQ , q  s '}
and  '( s ', )  {s | sˆs ' , s   ( sˆ,  )}
s’
Theorem: F and F’ have the same language.
q   (r , w)  q   '({r}, w)
Proof:
Finite State Machines as Automata
A FSM is M  ( S , I , O, T , r )
where I is the set of input symbols, O the set of output
symbols, r the initial state, and T(s,i,s’,o) is the transition
relation. A transition (s,i,s’,o) from state s to s’ with
output o can happen on input i can if and only if
( s, i, s ', o)  T ( s, i, s ', o)
If ( s, i )( s ', o)[( s, i, s ', o)  T ]
then M is complete, otherwise partial.
It is deterministic if for all (s,i) there is at most one (s’,o)
such that ( s, i, s ', o)  F
It is pseudo-non-deterministic if for all (s,i,o) there is at
most one s’ such that ( s, i, s ', o)  F
Converting an FSM to an automaton
An FSM M can be converted into an automaton F by the
following: F  ( S ,( I  O),  , r , S )
where  ( s, io)  {s ' | ( s, i, s ', o)  T }
Note that Q = S, i.e. all states are accepting
The resulting automaton is typically not complete, since
there are io combinations for which a next state is not
defined. We can complete it by augmenting 
to include a transition to a new non-accepting state DCN.
f
s
f
DCN
FSMs as Automata
The language of an FSM is defined to be the language of the
associated automaton
A pseudo non-deterministic FSM is one whose automaton
is deterministic.
The language of an FSM is prefix closed.
The language of an FSM is I-progressive
Conversion M  F
is done by grouping i/o on edges to (io) and making all
states accepting.
Conversion F  M
can be done only if the language is prefix closed and
I-progressive. In this case, delete all non-accepting states
(prefix), and change edges from (io) to i/o.
Computational Procedure
Computing the transition
relation of CSF
1. Complement S
Specification: S (i,o)
Context:
C (i,v,u,o)
(these have been
converted into automata)
S
2. Raise S to variables of C
3. Compose S with C
( S )( i ,v ,u ,o )
4. Hide variables not in X
(C ( S )( i ,v ,u ,o ) )( u ,v )
5. Complement result
(C ( S )( i ,v ,u ,o ) )( u ,v )
(C ( S )( i ,v ,u ,o ) )
Comparison with combinational case
Sequential
CSF (u, v)  i ,o (C ( S )( i ,v ,u ,o ) )( u ,v )
i
spec
context
u
o
v
unknown
Combinational
CF (Yi , yi )  X , Z [ M ( X , Yi ) R( X , yi , Z )]R spec ( X , Z )
  X , Z [ M ( X , Yi )  R ( X , yi , Z )
R( X , yi , Z )
X
M ( X , Yi )
Yi
yi
unknown
R
spec
( X , Z )]
Application - splitting FSM blif files
u
i
FSM
FSM1
o
v
FSM2
A run on s298.blif splitting 14 latches
into 7 each
mvsis 07> source langi.script
Extracting STG of spec ...
The extracted STG has 218 states and 1078 transitions.
Extracting STG of fixed ...
The extracted STG has 43 states and 128 transitions.
Extracting STG of particular solution ...
The extracted STG has 20 states and 400 transitions.
Determinizing the spec ...
The automaton is deterministic; determinization is not performed.
Computing the product ...
Product: (43 st, 128 trans) x (219 st, 1297 trans) -> (966 st, 9975 trans)
Determinizing the product and making progressive...
The automaton is deterministic; determinization is not performed.
Checking containment …
The solution composed with fixed is contained in the spec.
The particular solution is contained in the solution
mvsis 13> psa x.aut
x.aut: The automaton is incomplete (552 states) and deterministic.
mvsis 13> minimize x.aut x-min.aut
State minimization: (554 states, 5674 trans) -> (272 states, 2704 trans)
X-min.aut but not from splitting s298 (too big to show);
instead from splitting s27
The End