Abstract:
Ordered binary decision diagrams (OBDDs), which have been introduced
in 1986, provide the state-of-the-art data structure for representing Boolean
functions. Within the last decade, they have found
numerous applications, in particular in computer-aided design of integrated
circuits (CAD for VLSI) and in formal verification. OBDDs represent Boolean
functions by means of a decision process in a rooted
directed acyclic graph.
As the running times of all algorithms on OBDDs are correlated to the
size of the input graphs and of the resulting graphs, it is an important
task to optimize the size of these graphs. This topic has become even
more serious by the observation that for a substantial number of OBDD-based
applications the choice of the optimization technique is the deciding factor
whether a computation succeeds or not. The main
optimization parameter of OBDDs is the underlying variable order. Hence,
many research efforts have been spent to efficient optimization algorithms
for constructing good variable orders. Unfortunately, there are
many important applications, in particular in the analysis of finite
automata/finite state machines, where this optimization technique reaches
its limits.
In this thesis, we propose and discuss new optimization approaches for
decision diagrams. Our central topic is the use of transformation techniques
to reduce the size of OBDDs. In particular, we focus on two
concepts that are related to each other.
Encoding transformations: We systematically analyze and exploit the fact that in the context of finite state machines the state encoding can be used as an additional optimization parameter.
Domain transformations: Recently, the concept of domain transformations
has been proposed to enlarge the optimization space of variable ordering.
We characterize suitable classes of transformations and
show how these constructions can be well integrated into existing algorithms
for finding good variable orders. Here, it turns out that the class of
linear transformations is of particular importance.
Within this framework, we cover a variety of aspects: from theoretical
investigations over optimization algorithms, fully automated techniques,
implementation issues of efficient realizations, up to applications in
VLSI design. Our presentation shows that the proposed transformation
techniques significantly enrich the tool set of Boolean manipulation in
computer-aided circuit design.
Table of Contents
Introduction .......................................... 1
1. Basic Concepts ..................................... 7
1.1 Binary Decision Diagram ........................
7
1.1.1 Construction and Manipulation
............ 9
1.1.2 Implementation Techniques
................ 9
1.1.3 The Variable Order .......................
10
1.1.4 Local Variable Swaps
..................... 12
1.1.5 The Sifting Algorithm
.................... 13
1.2 Variants of OBDDs ..............................
15
1.2.1 Ordered Functional Decision
Diagrams ..... 15
1.2.2 Zero-Suppressed Binary
Decision Diagrams . 15
1.3 Transformed Binary Decision Diagrams ...........
16
1.4 Finite State Machines ..........................
18
1.5 Reachability Analysis ..........................
19
1.6 Relevant Software Systems ......................
20
1.6.1 The CUDD Package .........................
20
1.6.2 The SIS System ...........................
21
1.6.3 The VIS System ...........................
21
2. The Influence of the State Encoding ................ 23
2.1 Basic Framework ................................
24
2.2 The Lower Bound ................................
25
2.3 The Behavior of Important Encodings ............
27
2.3.1 The Standard Minimum-Length
Encoding ..... 27
2.3.2 The Gray Encoding ........................
30
2.4 A Worst-Case Encoding ..........................
31
2.5 Related Topologies .............................
37
2.6 Conclusion and Open Questions ..................
37
3. Local Encoding Transformations ..................... 39
3.1 Motivation: The Potential of Re-encoding .......
40
3.2 Local Re-encodings .............................
42
3.3 The XOR-Transformation .........................
43
3.3.1 Enumeration Results
...................... 44
3.3.2 Bounded Size Alteration
.................. 46
3.3.3 Stronger Bounds ..........................
46
3.3.4 General Two-Bit Re-encodings
............. 48
3.3.5 Implementation Aspects
................... 49
3.4 Who Profits From XOR ?..........................
50
3.5 Experimental Results ...........................
52
3.6 Conclusion .....................................
53
3.7 Two Proofs .....................................
53
4. Linear Sifting ..................................... 57
4.1 Preliminaries ..................................
58
4.2 Linear Sifting .................................
59
4.3 Experimental Results ...........................
63
4.4 Conclusion .....................................
64
5. Function Decomposition and Technology Mapping ..... 67
5.1 Synthesis by Spectral Analysis .................
68
5.2 Synthesis by Linear Sifting ....................
70
5.3 Experimental Results ...........................
71
5.4 Linear Sifting and Adder Functions .............
76
5.4.1 Adder Behavior ...........................
78
5.4.2 The ISOP Algorithm .......................
82
5.4.3 Open Questions ...........................
88
6. Related Approaches and Final Remarks ............... 91
6.1 Related Approaches .............................
91
6.2 Final Remarks ..................................
92
