Hardware Reference
In-Depth Information
derived, and thus, for example, state duplication is not allowed. Therefore, solutions
which would circulate around a loop a finite number of times before leaving the
loop would not be captured.
7
In addition, as mentioned already, in the general case,
we may have lost some solutions (in case
S
in not co-looping) by using the subset
construction on
P
#
.
u
;
v
/
.
18.4.2.1
SAT Formulation
The deterministic co-Buchi solution
P
#
.
u
;
v
/
will be trimmed so that the only
cycles left are those entirely contai
ned in
the stable set
C
. This requires removing
transitions (edges) in the graph of
P
#
.
u
;
v
/
making the non-stable part acyclic but
still maintaining
u
-progressiveness (
u
is the only input for the unknown component
shown in Fig.
18.1
). This is formulated as a SAT instance where each satisfying
assignment will correspond to a way of trimming the graph to give to the sub-graph
the desired property.
For each transition
j
!
k
,avariable
e
jk
D
1
if the transition is chosen to
remain. For each state
j
,avariable
s
j
D
1
if
j
is chosen to remain.
Let
E
j
u
be the set of edges that may be traversed on input
u
in one step from state
j
.
E
j
u
D
e
j1
C
:::e
jn
,where
n
is the cardinality of
E
j
u
.The
u-progressiveness
u
clauses
,
j
D
E
j
u
, say that for input
u
, there exists at least one next state. Thus,
the
u
-progressiveness of state
C
j
is
C
j
D
.s
j
)
˘
u
E
j
u
/
, which says that if state
j
is selected, then it must be
u
-progressive, meaning that for each minterm of
u
,
there exists a next state.
Connection clauses
, say that if edge
e
ij
is selected, then
C
ij
D
.e
ij
)
s
i
/.e
ij
)
s
j
/
both terminal states have to be selected, i.e.
. Finally, to
eliminate every simple loop not entirely contained in the stable set,
loop-breaking
clauses
are constructed, one for each such loop. Suppose
L
Df
e
12
;e
23
;e
34
;:::;e
l1
g
is such a loop. Its loop-breaking clause says tha
t at
le
ast
on
e o
f these tr
an
sitions
should not be chosen. This is equivalent to
C
L
D
e
12
C
e
23
C
e
34
CC
e
l1
.
We must also require that the initial state
s
0
be selected. Thus,
C
0
D
s
0
,i.e.,
s
0
D
1
, is added as an assumption.
Since all simple unstable loops must be enumerated, there could be many such
loops. To alleviate this problem, the graph is pre-processed to eliminate certain
obvious transitions, using the notion of essential edges. This is described below.
This reduction usually cuts down the number of loops considerably.
Summing up, any solution is a selection of a subset of states and transitions of
P
.
This corresponds to a sub-graph of the most general solution
where every state is
u
-progressive and in the graph there is no loop not entirely contained in
X
.Being
u
-progressive means that the graph represents a (possibly non-deterministic) FSM.
C
7
It might be argued that such solutions are impractical since they simply delay getting to the stable
set.
Search WWH ::
Custom Search