ECCC BOOKS, LECTURES AND SURVEYS > ALGORITHMS AND DATA STRUCTURES IN VLSI DESIGN TABLE OF CONTENT:
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
