Information Technology Reference
In-Depth Information
Algorithm 1.
The safe-state synthesis algorithm.
1:
input
:
Q
x
,Q
S
0
2:
let
X
0
:=
Q
x
,k
:= 0;
3:
repeat
4:
k
:=
k
+1;
5:
Q
:= RestrictedBackward(
Q
m
,X
k−
1
);
6:
Q
:= UncontrollableBackward(
Q
S
0
\Q
);
7:
X
k
:=
X
k−
1
∪
(
Q
);
8:
until
X
k
=
X
k−
1
9:
return
Q
S
0
\X
k
4.1
Efficient State Space Search
Not surprisingly, the backward and forward reachability searches turn out to be the
bottle-neck of the algorithm presented above. The problem with the intuitive reachabil-
ity is that for a large and complicated modular DES, the BDD representation of the total
transition function
δ
S
0
is often too large to be constructed. The natural way to tackle
the complexity of the transfer function is to split it into a set of less complex partial
functions with a connection between them. Such methods are based on conjunctive and
disjunctive partitioning techniques.
Conjunctive Representation.
Conjunctive partitioning, introduced in [14,15], is an
approach to represent synchronous digital circuits where all transitions happen simul-
taneously. In the context of DES, the conjunctive partitioning of the full synchronous
composition can be achieved by adding self-loops to the automata for events that are not
included in their original alphabets. This leads to a situation where all automata have
equal alphabet. Therefore, the conjunctive transition function
δ
i
for the automaton
A
i
and the total transition function can be defined as follows:
⎧
⎨
δ
i
(
q
i
,σ
) f
δ
i
(
q
i
,σ
) is defined
q
i
δ
i
(
q
i
,σ
)=
Σ
i
undefined otherwise
.
if
σ/
∈
(2)
⎩
δ
=
1
≤i≤n
δ
i
.
(3)
By making use of (2) and (3), we can search the state-space without constructing the
total transition function. Algorithm 2 applies this technique for the forward reach-
ability search. Assuming that the automaton set
A
=
{
A
1
,...,A
n
}
and the state
q
1
,q
2
,...,q
n
q
=
, the algorithm explores the target state
q
by performing each con-
junctive transition function
δ
i
with arguments (the local state
q
i
and the event
σ
∈
Σ
)
to get each local target state
q
i
.
Disjunctive Representation.
The conjunctive partitioning of the transition relation
works well for formal verification of synchronous digital circuits. However, because of
the asynchronous feature of the full synchronous composition, the intermediate states
(
Q
k−
1
) can still cause the explosion problem when performing the reachability search,
