Christoph Meinel, Universität Trier
Thorsten Theobald, Technische Universität München
Algorithms and Data Structures in VLSI Design:
OBDD - Foundations and Applications
Contents
1. Introduction
2. Basics
2.1 Propositions and Predicates -
2.2 Sets, Relations, and Functions -
2.3 Graphs -
2.4 Algorithms and Data Structures -
2.5 Complexity of Algorithms -
2.6 Hashing -
2.7 Finite Automata and Finite State Machines -
2.8 References
Part I: Data Structures for Switching Functions
3. Boolean Functions
3.1 Boolean Algebras - 3.2 Boolean Formulas and Boolean Functions -
3.3 Switching Functions -
3.3.1 Switching Functions with at most Two Variables -
3.3.2 Subfunctions and Shannon's Expansion -
3.3.3 Visual Representation -
3.3.4 Monotone Switching Functions -
3.3.5 Symmetric Functions -
3.3.6 Threshold Functions -
3.3.7 Partial Switching Functions -
3.4 References
4. Classical Representations
4.1 Truth Tables -
4.2 Two-Level Normal Forms -
4.3 Circuits and Formulas -
4.3.1 Circuits -
4.3.2 - Formulas -
4.4 Binary Decision Trees and Diagrams -
4.4.1 Binary Decision Trees -
4.4.2 Branching Programs -
4.4.3 Read-Once Branching Programs -
4.4.4 Complexity of Basic Operations -
4.5 References
5. Requirements on Data Structures in Formal Circuit Verification
5.1 Circuit Verification -
5.2 Formal Verification of Combinational Circuits -
5.3 Formal Verification of Sequential Circuits -
5.4 References
Part II: OBDDs: An Efficient Data Structure
6. OBDDs - Ordered Binary Decision Diagrams
6.1 Notation and Examples -
6.2 Reduced OBDDs: A Canonical Representation of Switching Functions -
6.3 The Reduction Algorithm -
6.4 Basic Constructions -
6.5 Performing Binary Operations and the Equivalence Test -
6.6 References
7. Efficient Implementation of OBDDs
7.1 Key Ideas -
7.1.1 Shared OBDDs -
7.1.2 Unique Table and Strong Canonicity -
7.1.3 ITE Algorithm and Computed Table -
7.1.4 Complemented Edges -
7.1.5 Standard Triples -
7.1.6 Memory Management -
7.2 Some Popular OBDD Packages -
7.2.1 The OBDD Package of Brace, Rudell, and Bryant -
7.2.2 The OBDD Package of Long -
7.2.3 The CUDD Package: Colorado University Decision Diagrams -
7.3 References
8. Influence of the Variable Order on the Complexity of OBDDs
8.1 Connection Between Variable Order and OBDD Size -
8.2 Exponential Lower Bounds -
8.3 OBDDs with Different Variable Orders -
8.4 Complexity of Minimization -
8.5 References
9. Optimizing the Variable Order
9.1 Heuristics for Constructing Good Variable Orders -
9.1.1 The Fan-In Heuristic -
9.1.2 Die Weight Heurisitic -
9.2 Dynamic Reordering -
9.2.1 The Variable Swap -
9.2.2 Exact Minimization -
9.2.3 Window Permutation -
9.2.4 The Sifting Algorithm -
9.2.5 Block Sifting and Symmetric Sifting -
9.3 Quantitative Statements -
9.4 Outlook -
9.5 References
Part III: Applications and Extensions
10. Analysis of Sequential Systems
10.1 Formal Verification -
10.2 Basic Operators -
10.2.1 Generalized Cofactors -
10.2.2 The Constrain Operator -
10.2.3 Quantification -
10.2.4 The Restrict Operator -
10.3 Reachability Analysis -
10.4 Efficient Image Computation -
10.4.1 Input Splitting -
10.4.2 Output Splitting -
10.4.3 The Transition Relation -
10.4.4 Partitioning the Transition Relation -
10.5 References
11. Symbolic Model Checking
11.1 Computation Tree Logic -
11.2 CTL Model Checking -
11.3 Implementations -
11.3.1 The SMV System -
11.3.2 The VIS System -
11.4 References
12. Variants and Extensions of OBDDs
12.1 Relaxing the Ordering Restriction -
12.2 Alternative Decomposition Types -
12.3 Zero-Suppressed BDDs -
12.4 Multiple-Valued Functions -
12.4.1 Additional Sinks -
12.4.2 Edge Values -
12.4.3 Moment Decompositions -
12.5 References
13. Transformation Techniques for Optimization
13.1 Transformed OBDDs -
13.2 Type-Based Transformations -
13.2.1 Definition -
13.2.2 Circuit Verification -
13.3 Linear Transformations -
13.3.1 Definition -
13.3.2 Efficient Implementation -
13.3.3 Linear Sifting -
13.4 Encoding Transformations -
13.5 References
Bibliography
Index
Back to the main page of the book