Local Encoding Transformations for Optimizing OBDD-Representations of Finite State Machines.
Ordered binary decision diagrams are the state-of-the-art representation of switching functions. In order to keep the sizes of OBDDs tractable, heuristics and dynamic reordering algorithms are applied to optimize the underlying variable order. When finite state machines are represented by OBDDs the state encoding can be used as an additional optimization parameter. In this paper, we analyze local encoding transformations which can be applied dynamically. First, we investigate the potential of re-encoding techniques. We then propose the use of an XOR-transformation and show why this transformation is most suitable among the set of all encoding transformations. The presented theoretical framework establishes a new optimization technique for OBDDs.
Introduction
Ordered binary decision diagrams (OBDDs) which have been introduced by Bryant [Bry86]
provide an efficient graph-based data structure for switching functions. The main optimization
parameter of OBDDs is the underlying variable order. In order to find a good order
two techniques were applied so far: the use of heuristics which try to exploit the structure of
a circuit representation (see e.g. [MWBS88]), and dynamic reordering techniques [Rud93].
Unfortunately, there are many applications, in particular in the field of sequential analysis,
where these two optimization techniques for OBDDs reach their limits. Hence, one essential
problem in logic synthesis and verification is to find new techniques to minimize OBDDs in
these applications.
When OBDDs are used to represent finite state machines the OBDD-size does not only
depend on the variable order but also on the state encoding. For a fixed state encoding there
are many finite state machines whose OBDD-representations are large w.r.t. all variable orders
[ATB94]. Therefore the relationship between the OBDD-size and the state encoding
becomes of increasing interest, see e.g. [QCC The importance of this relationship
is underlined by recent ideas to apply heuristic state re-encoding techniques to speed
up a verification process between similar-structured finite state machines [QCC
The underlying general problem of all these efforts is the following: Given the OBDDs
for the next-state and output functions of a finite state machine - if one is interested in
the input/output behavior of the machine, in how far can the internal state encoding be
exploited to minimize OBDD-sizes ? Our approach targets at applying local encoding trans-
formations, i.e. transformations which involve only a limited number of encoding bits. These
in: Proceedings FMCAD'96, LNCS
Supported by DFG-Graduiertenkolleg "Mathematische Optimierung".
transformations can be interpreted as a re-encoding of the symbolic states. The aim is to
minimize OBDD-sizes by the iterated application of local transformations. The advantage
of this approach is that the costs for applying these transformations are still manageable.
The paper is structured as follows: We begin with recalling some important definitions
and point out the principle potential of state re-encodings w.r.t. OBDD-sizes. Then, in
Section 4, we analyze the advantages of local encoding transformations. In Section 5 we
propose the application of the XOR-transformation and show why this transformation is
most promising among the set of all encoding transformations. At the end of the paper we
describe an implementation of this transformation and give some first experimental results
which illustrate the positive impact of the presented ideas.
Preliminaries
2.1 Finite state machines
a finite state machine, where Q is the set of states, I the input
alphabet, O the output alphabet,
the output function and Q 0 the set of initial states. As usual, all components of the state
machine are assumed to be binary encoded. Let p be the number of input bits, n be the
number of state bits and m be the number of output bits. In particular, with
is a function IB n \Theta IB p ! IB n ,  is a function IB n \Theta IB p ! IB m , and Q 0 is a subset of IB n .
2.2 Binary decision diagrams
Ordered binary decision diagrams (OBDDs) [Bry86] are rooted directed acyclic graphs representing
switching functions. Each OBDD has two sink nodes which are labeled 1 and 0.
Each internal node is labeled by an input variable x i and has two outgoing
edges, labeled 1 and 0 (in the diagrams the 1-edge is indicated by a solid line and the 0-edge
by a dotted line). A linear variable order  is placed on the input variables. The variable
occurrences on each OBDD-path have to be consistent with this order. An OBDD computes
a switching function f : IB n ! IB in a natural manner: each assignment to the input
variables x i defines a unique path through the graph from the root to a sink. The label of
this sink defines the value of the function on that input.
The OBDD is called reduced if it does not contain any vertex v such that the 0-edge and
the 1-edge of v leads to the same node, and it does not contain any distinct vertices v and
v 0 such that the subgraphs rooted in v and v 0 are isomorphic. It is well-known that reduced
OBDDs are a unique representation of switching functions f with respect to
a given variable order [Bry86]. The size of an OBDD is the number of its nodes. Several
functions can be represented by a multi-rooted graph called shared OBDD. In the following,
all next-state and output functions are represented by a shared OBDD.
2.3 The transition relation
For a finite state machine M , the characteristic function of its transition relation is defined
by
Y
1in
Hence, the function T computes the value 1 for a triple (x; only if the state
machine in state x and input e enters the state y. The variables x are called
current-state variables and the variables y are called next-state variables.
3 Motivation: The Potential of Re-encoding
In order to demonstrate how much the size of an OBDD-representation depends on the
choice of the state encoding, let us consider an autonomous counter, a finite state machine
with a very simple structure:
Example 1. An autonomous counter (see for example [GDN92]) with 2 n states q
is an autonomous (i.e. input-independent) finite state machine with ffi(q i

Figure

1: Autonomous counter
ae
oe
ae
oe
ae
oe
ae
oe
ae
oe
Transitions: input/output
The following theorem shows that almost all encodings for the autonomous counter lead
to exponential-size OBDDs, even for their optimal variable order.
Theorem 1. Let e(n) denote the number of n-bit encodings for the autonomous counter
with 2 n states which lead to a (shared) OBDD of size at most 2 n =n w.r.t. their optimal
variable order. Let denote the number of all possible counter encodings. Then
the ratio e(n)=a(n) converges to zero as n tends to infinity.
The proof of the theorem can be found in the appendix. It is based on ideas of [LL92]
and classical counting results of Shannon [Sha49]. An analogous result can be established
for the characteristic function of the transition relation and its OBDD-size.
Definition 2. An encoding transformation, shortly called a re-encoding, is a bijective
that transforms the given state encoding to a new encoding. (For an
example see Figure 2.) If a state s is encoded by a bit-string c 2 IB n , then its new encoding
is ae(c).

Figure

2: Encoding transformation ae(c
original new
state encoding encoding
q3
1=0
1=0
1=0
new: 11
This modification of the internal state encoding does not modify the input/output
behavior of the state machine. The machine with the new encoding is denoted by
Its encoded next-state function, output function and set of initial
states are computed as follows:
The transition relation of the re-encoded machine M 0 can be obtained from the transition
relation of M as follows:
Lemma 3. Let T (x; be the characteristic function of the transition relation of M .
Then the characteristic function T 0 (x; of the transition relation of M 0 is
Y
ae
Therefore can be obtained from T (x; by the substitutions y i
Proof. The lemma is a consequence of the following equivalences:
ae
Example 1 (ctd. The large potential of re-encoding techniques can now be demonstrated
at the example of the autonomous counter: There exists an encoding such that the transition
relation of the autonomous counter with 2 n states and n encoding bits has at most 5n \Gamma 1
nodes [TM96] even if the variable order is fixed to x Hence, for each given
encoding of a finite state machine, there exists a re-encoding which leads to OBDDs of linear
size. As according to Theorem 1 most encodings lead to OBDDs of exponential size, the
gain between the original OBDD and the OBDD after a suitable re-encoding is exponential
in most cases. The aim now is to find the suited re-encoding that leads to small OBDD-sizes.
In the previous section we have shown that re-encodings may have a large impact on the
OBDD-size. It is possible that the OBDD becomes much smaller, but in the case of a badly
chosen re-encoding the OBDD could even become much larger. This situation is comparable
to the problem of finding a good variable order for an OBDD. When changing the variable
order of an OBDD, the graph may become much smaller in the best case or much larger in
the worst case. This sensitivity is the main reason why it is hard to find a good re-encoding
or a good variable order.
For the effective construction of good variable orders it has turned out that the most
efficient strategies are based on local exchanges of variables. The presently best strategies
for finding good variable orders dynamically are based on the sifting algorithm of Rudell
[Rud93, PS95]. The main principle of this algorithm is based on a subroutine which finds
the optimum position for one variable, if all other variables remain fixed. This subroutine is
repeated for each variable. There are two main reasons why this strategy works so efficiently:
Bounded size alteration: If one variable x i is moved to another position in the OBDD,
the size of the OBDD cannot change arbitrarily much, in particular it cannot explode.
[BLW95] have shown the following theorem:
Theorem 4. Let P be an OBDD. If a variable x i is moved to a later position in the
variable order, then the size of the resulting OBDD P 0 satisfies
If a variable x i is moved to an earlier position in the variable order, then the size of
the resulting OBDD P 0 even satisfies the relation
Practical studies have shown that in most cases the resulting sizes are even far below
the worst-case estimations. Hence, each application of the above mentioned subroutine
keeps the size of the OBDD manageable. However, this bounded size alteration for
the subroutine does not mean that the optimization potential is limited. The iteration
of this subroutine allows to minimize OBDDs very effectively.
Continuity: The procedure for moving a variable x i to a different position in the order
works continuously: During this process only the variables between the original and
the new position of x i are involved, and all nodes labeled by the remaining variables
remain untouched. In particular, the time complexity of this operation is very small
if x i is moved to an adjacent position, and it increases with the number of variables
between the original and the new position of x i in the variable order.
In the case of re-encoding the situation is analogous. It seems to be very hard to find
the right global re-encoding, whereas it is very promising to combine and iterate operations
with restricted local effect. Our approach to construct local re-encodings ae : IB n ! IB n is
to keep most of the bits fixed (i.e. ae i vary only on a small number of bits.
In particular, if we vary only 2 bits, we will speak of two-bit re-encodings. In this case it
follows from the worst-case bounds for the synthesis and the substitution of OBDDs that
the OBDDs remain polynomial.
Example 2. The exchange variables re-encoding ae
follows (The following definition shows the case i ! j, the case i ? j is defined
Obviously, the exchange variables re-encoding has the same effect on the next-state functions
as exchanging the state variables x i and x j in the variable order. From all the (2 n )!
possible encoding transformations n! can be generated by the iterated application of this
transformation type. The inverse mapping ae \Gamma1 from Equation 1 does not affect the size of
the resulting OBDDs as this mapping only causes the renaming of the two functions
Note, that the transformation which exchanges the encodings of two fixed states may
not be seen as a local operation, although the transformation seems to be very simple.
5 The XOR-Transformation
We will now propose XOR-transformations. This transformation is a local re-encoding which
operates on two bits.
Definition 5. An XOR-transformation ae i;j , 1
Short . For an example see Figure 3.

Figure

3: The XOR-transformation q 1 7! q 1 \Phi q 2
original new
encoding encoding
q1 q2 q new
Indeed, XOR-transformations provide a solid basis for the design of effective re-encodings
due to the following facts:
1. The number of possible re-encodings generated by the iterated application of XOR-
transformations is much larger than the number of possible variable orders. Thus,
XOR-transformations considerably enlarge the optimization space. On the other hand,
the number of these re-encodings is much smaller than the number of all re-encodings
which makes it possible to keep the search space manageable.
2. The size influence of this transformation is bounded in a reasonable way like in the
case of local changes in the variable order.
3. A precise analysis even shows that an XOR-transformation contains the same asymmetry
as the movement of one variable in the variable order. Namely, the bounds for
the effect of a transformation x i 7! x i \Phi x j depends on the position of x i and x j in the
variable order.
4. The XOR-transformation is in fact the only new possible re-encoding on two variables.
5. The XOR-transformation can be implemented efficiently like an exchange of two variables
in the order.
In the following subsection we will prove these statements.
5.1 Enumeration results
The following combinatorial statements characterize the size of the optimization space provided
by the use of XOR-transformations.
Lemma 6. (1) Let t(n) be the number of possible encoding transformations that can be
generated by the iterated application of XOR-transformations. It holds
(2) The quotient of t(n) and the number of all possible encoding transformations converges
to zero as n tends to infinity.
(3) Let v(n) := (2n)! denote the number of possible variable orders for the transition relation
of an autonomous finite state machine with n state bits. The fraction v(n)=t(n) converges
to zero as n tends to infinity.
Statement 3 says that in the case of autonomous state machines, there are much more
encoding transformations generated by XOR-transformations than variable orders for the
transition relation. This relation also holds when the number of input bits is fixed and the
number of state bits becomes large.
Proof. (1) Obviously, each XOR-transformation is a regular linear variable transformation
over the field ZZ 2 . Moreover, the XOR-transformations provide a generating system for all
regular linear variable transformations. Therefore the state encodings which can be obtained
by iterated XOR-transformations are in 1-1-correspondence with the regular n \Theta n-matrices
over ZZ 2 .
The number of these matrices can be computed as follows: The first row vector b 1 can be
chosen arbitrarily from ZZ n
The i-th row vector b i , 2  i  n, can be chosen arbitrarily
from
These are 2 possibilities for the vector b i . This proves the claimed number.
(2) This statement follows from the relation
(3) It holds
!1:In particular, the number of possible encoding transformations which can be generated
by the iterated application of XOR-transformations is smaller than 2
which is exactly the
number of all n \Theta n-matrices over ZZ 2 .
It follows from the previous proof that all exchanges of two state variables can be simulated
by the iterated application of XOR-transformations.
5.2 Bounded size alteration
Let ae be the XOR-transformation q i 7! q i \Phi q j . Then the inverse transformation is defined
by
i.e. we have . The effect of ae(ffi(ae \Gamma1 (\Delta))) in Equation 1 can be split into two parts:
1. Substitute the current-state variable x i by x i \Phi x j .
2. Replace the function ffi i by
It does not matter which of these two steps is executed first.
Lemma 7. Let P be the OBDDs for
n be the OBDDs after
the application of the XOR-transformation q i 7! q i \Phi q j . The following holds:
The upper bound immediately follows from the facts that the substitution of an OBDD P 2
into one variable of an OBDD P 1 leads to an OBDD of size at most O(size(P 1
and that the operation P 1 \Phi P 2 leads to an OBDD of size at most O(size(P 1
the lower bounds it suffices to observe
In case of the transition relation both the current-state variables and the next-state
variables have to be substituted. This leads to the result
where P and P 0 are the original and the re-encoded OBDD for the transition relation,
respectively.
5.3 Stronger bounds
For a more refined analysis of the XOR-transformation we use the following theorem from
[SW93]. In particular, we will refine the analysis for the substitution of a variable x i by
in an OBDD.
Theorem 8. The reduced OBDD representing f with the variable order x contains
as many x i -nodes as there are different functions f S , S ae depending essentially
on x i (i.e. f S
where a
otherwise. 2
Let s k be the number of nodes labeled by x k in the OBDD P and s
k be the number of
nodes labeled by x k in the OBDD P 0 which is the result of the transformation.
Theorem 9. The size of an OBDD w.r.t. the variable order x after the application
of the substitution x i 7! x i \Phi x j is bounded from above by
and by
The proof of this theorem can be found in the appendix. It applies ideas from [BLW95],
in which local changes in the variable order are analyzed.
Corollary 10. Let P be an OBDD and P 0 the resulting OBDD after the substitution x i 7!
The analogy between the behavior of the XOR-transformation and the local changes in
the variable order recommends to use XOR-transformations for the optimization of OBDD-
sizes.
The XOR-transformation x i 7! x i \Phi x j for can be visualized as
shown in Figure 4. Let A and B be the two sub-OBDDs whose roots are the children of an
Consider a path from x j to x i . If this path contains the 0-edge of x j , the subgraph
rooted in x i remains unchanged. If instead the path contains the 1-edge of x j , the 0- and
the 1-successor of the x i -node are exchanged. This modification can prevent subgraph-
isomorphisms in the new sub-OBDDs which are rooted in an x k -node,

Figure

4: Mutation x i 7! x i \Phi x j for x
(a) path along 0-edge of x j
remains
unchanged
(b) path along 1-edge of x j
5.4 General two-bit re-encodings
The effect of each two-bit re-encoding can be split into the two-parts "Substitute the two
variables x i and x j by some functions" and "replace the two functions
functions". The variable substitution has an impact on all functions which depend essentially
on x i or x j , whereas the function replacement only affects the functions ffi
The next table shows that all re-encodings which are induced by the bijective
can be obtained by a combination of maximal one XOR-
transformation, an exchange variable transformation and the identity. Hence, beside the
exchange variable transformation merely XOR-transformations are needed to produce all
two-bit re-encodings. We write a two-bit re-encoding which is induced by f as
ae f
22
The substitution x i 7! x i does not affect the size of the OBDD. As x i \Phi x
each of the above 24 transformations has the same effect w.r.t. the OBDD-size as
a combination of the exchange variables transformation, the XOR-transformation and the
identity operation. Moreover, for each of the 24 transformations, a combination of at most
two of the "basis" transformations suffices.
Implementation aspects
In this section we will describe how to implement the XOR-substitution x i 7! x i \Phi x j
efficiently. Our starting point is the consideration of local changes in the variable order. In
order to modify the variable order of OBDDs we iterate exchanging variables in adjacent
levels. Since an exchange of adjacent variables is a local operation consisting only of the
relinking of nodes in these two levels, this can be done efficiently as shown in Figure 5. In
order to move a variable x i behind an arbitrary variable x j in the order, the exchanges of
adjacent variables are iterated.

Figure

5: Exchanging two neighboring variables
Level exchange
In case of the XOR-operation and adjacent variables x i and x j , we can proceed analogous
to the level exchange. Figure 6 shows the case where x j is the direct successor of x i in the
order. The case where x i is the direct successor of x j in the order works analogously. If x i
and x j are not adjacent, it would of course be helpful if we could simulate the substitution
by a sequence like x i 7! x i \Phi x
this straightforward idea does not work, as this would require operations in the intermediate
steps which influence more than two adjacent levels.

Figure

Performing x i 7! x i \Phi x j for two neighboring variables x i , x j
r h g s
A method that works and is only slightly more expensive than the exchange of two non-adjacent
variables is the following: First, shift the variable x i to a new position in the order
which is adjacent to x j . Then perform the XOR-operation, and then shift the variable x i
back to its old position. This technique retains the locality of the operation, as only nodes
with a label x k are influenced whose position in the order is between x i and x j .
6 Do All FSM-Descriptions Profit From XOR-Re-encodings?
In principle, the applicability of the XOR-transformation is not restricted to the use of
OBDDs as underlying data structure. It can also be applied to other data structures for
Boolean functions. However, the strong relationship between the XOR-transformation and
local changes in the variable order like in the case of OBDDs does not always transfer to
other representations. We will demonstrate this effect on OFDDs.
Ordered functional decision diagrams (OFDDs) [KSR92] are a modification of OBDDs
which seem to be more compact for arithmetic functions. Each node v with label x i in an
OBDD represents a Shannon decomposition
whereas each node v with label x i in an OFDD represents a Reed-Muller decomposition
In both decompositions the functions g and h are independent of x i and are the functions
which are represented by the subgraphs rooted in the two successor nodes of v.
It has been shown in [BLW95] that local changes in the variable order have the same
effect on OFDDs like on OBDDs. In particular, the exchange of two variables x i and x j in
the order only affects the nodes of an OBDD resp. OFDD which are labeled by a variable
whose position in the order is between x i and x j . These observations justify the notions
of local changes. From the proof of Theorem 9 it follows that the XOR-transformation for
OBDDs has also this pleasant local property. However, in spite of the fact that the Reed-Muller
decomposition seems to operate well with XOR-transformations, the substitution
does not have the local property like in the case of OBDDs.

Figure

7: OFDD for
x1 .
To prove this statement, consider the OFDD in Figure 7 which represents the function
for some functions independent of x . The function f 0
s:
Hence, there must exist a node in the OFDD for f 0 representing the function h \Phi r \Phi s. As
h, r and s are arbitrary functions, the substitution operation x i 7! x i \Phi x j does not have
the local property. However, as the \Phi-operation is a polynomial operation on OFDDs, the
result of the substitution remains polynomial.
A tight relationship between our re-encoding techniques and specific OBDD-variants is
the following: In a more general setting, the concept of domain transformations has been
proposed for the manipulation of switching functions [BMS95, FKB95]. The corresponding
variants of OBDDs are called TBDDs. In the following we show that our encoding
transformations can also be interpreted as TBDD-transformations.
IB be a switching function, and let  : IB n ! IB n be
a bijective mapping. A -TBDD-representation of f is an OBDD-representation of f ffi  ,
where ffi denotes the composition of functions.
It turns out that every re-encoding function ae defines a transformation within the TBDD-
concept. However, the OBDDs for the next-state functions of a re-encoded machine with
re-encoding function ae are not isomorphic to the ae-TBDDs, as in the OBDDs of the re-encoded
machine, the transformation ae \Gamma1 is also involved (see Equation (1) in section 3).
7 Experimental Results
In this section we present some very first experimental results on the extended optimization
techniques for OBDDs. We built up some routines on top of the OBDD-package of D. Long
and used the ISCAS89 benchmark circuits s1423, s5378, s9234 which have a large number
of state bits and have also formed the set of examples in [RS95]. Each optimization run
consists of three phases: First, we applied Rudell's sifting algorithm [Rud93] for finding a
good variable order. Then some minimization based on XOR-transformations is performed.
Finally, sifting is applied once more to re-establish a suitable variable order. The table shows
the obtained shared OBDD-sizes of the next-state functions in comparison to the sizes that
were obtained without the minimization by XOR-transformations.
without with
Circuit # state bits XOR XOR
The minimization based on XOR-transformation works as follows: In a preprocessing
step we compute promising pairs (i; j) for an XOR-transformation. The heuristic criteria
for considering a pair (i; j) as promising are:
1. the next-state functions have a nearly equal support, or
2. the variables x i and x j appear in nearly the same functions.
Then, as long as improvements are possible, the best XOR-transformation among these
pairs are applied. In order to avoid the expensive computations
this step if the variable substitution x i 7! x i \Phi x j yields a good intermediate result.
It must be admitted that in our experiments, the running times are significantly higher
than the running times for pure sifting. This is due to a non-optimal implementation of
the XOR-transformation and due to the large number of performed XOR-transformations.
However, we think that intensive studies of different strategies (analogous to the intensive
and finally quite successful studies of the variable order) should be able to improve these
results by far. Hence, we think that these experimental results underline the optimization
potential of the XOR-transformation.
An efficient implementation of the XOR-transformation and the construction of effective
minimization strategies is in progress.
8 Conclusion and Future Work
We have proposed and analyzed new re-encoding techniques for minimizing OBDDs. In
particular, we have proposed the XOR-transformation and shown that this transformation
is in fact the only new transformation on two state variables. This transformation can in
certain cases significantly enrich the set of basic operations for the optimization of OBDDs.
In the future we propose to study heuristics for choosing the right transformation pairs
and efficient combinations of variable reordering techniques with the new proposed trans-
formations. Furthermore, the dynamic application of the new re-encoding technique in the
traversal of a finite state machine seems promising: It helps to reduce the OBDD-sizes for
the set of reached states and also to reduce the efforts of the image computations.
9

Acknowledgements

We wish to thank Stefan Krischer, Jan Romann, Anna Slobodov'a and Fabio Somenzi for
interesting discussions and many valuable comments.



--R

BDD variable ordering for interacting finite state machines.
Simulated annealing to improve variable orderings for OBDDs.


BDD minimization by truth table permutations.
Sequential Logic Testing and Verifi- cation
Multilevel logic synthesis based on functional decision diagrams.
On the OBDD-representation of general Boolean functions
Logic verification using binary decision diagrams in a logic synthesis environment.
Who are the variables in your neighborhood.
Incremental FSM re-encoding for simplifying verification by symbolic traversal

Dynamic variable ordering for ordered binary decision diagrams.
The synthesis of two-terminal switching circuits

State encodings and OBDD-sizes
--TR
Graph-based algorithms for Boolean function manipulation
Sequential logic testing and verification
On the OBDD-Representation of General Boolean Functions
BDD variable ordering for interacting finite state machines
Efficient OBDD-based boolean manipulation in CAD beyond current limits
Who are the variables in your neighborhood
Dynamic variable ordering for ordered binary decision diagrams
Linear sifting of decision diagrams
Algorithms and Data Structures in VLSI Design
On the Influence of the State Encoding on OBDD-Representations of Finite State Machines

--CTR
Carla Piazza , Alberto Policriti, Ackermann encoding, bisimulations and OBDDs, Theory and Practice of Logic Programming, v.4 n.5-6, p.695-718, September 2004
local transformation;OBDD;state encoding;finite state machine;ordered binary decision diagram