Algorithms and Data Structures in Vlsi Design

by Meinel, Christoph; Theobald, Thorsten

• ISBN13: 9783540644866
• ISBN10: 3540644865
• Format: Paperback
• Copyright: 1998-10-01
• Publisher: Springer Verlag

Summary

One of the main problems in chip design is the huge number of possible combinations of individual chip elements, leading to a combinatorial explosion as chips become more complex. New key results in theoretical computer science and in the design of data structures and efficient algorithms, can be applied fruitfully here. The application of ordered binary decision diagrams (OBDDs) has led to dramatic performance improvements in many computer-aided design projects. This textbook provides an introduction to the foundations of this interdisciplinary research area with an emphasis on applications in computer-aided circuit design and formal verification.

Table of Contents

1. Introduction	1	(6)
2. Basics	7	(18)
2.1 Propositions and Predicates	7	(2)
2.2 Sets, Relations, and Functions	9	(2)
2.3 Graphs	11	(2)
2.4 Algorithms and Data Structures	13	(2)
2.5 Complexity of Algorithms	15	(4)
2.6 Hashing	19	(1)
2.7 Finite Automata and Finite State Machines	20	(2)
2.8 References	22	(3)
Part I. Data Structures for Switching Functions	25	(64)
3. Boolean Functions	25	(26)
3.1 Boolean Algebra	26	(4)
3.2 Boolean Formulas and Boolean Functions	30	(4)
3.3 Switching Functions	34	(15)
3.3.1 Switching Functions with at Most Two Variables	36	(2)
3.3.2 Subfunctions and Shannon's Expansion	38	(2)
3.3.3 Visual Representation	40	(1)
3.3.4 Monotone Switching Functions	41	(3)
3.3.5 Symmetric Functions	44	(3)
3.3.6 Threshold Functions	47	(1)
3.3.7 Partial Switching Functions	48	(1)
3.4 References	49	(2)
4. Classical Representations	51	(26)
4.1 Truth Tables	52	(1)
4.2 Two-Level Normal Forms	53	(7)
4.3 Circuits and Formulas	60	(3)
4.3.1 Circuits	60	(2)
4.3.2 Formulas	62	(1)
4.4 Binary Decision Trees and Diagrams	63	(12)
4.4.1 Binary Decision Trees	64	(2)
4.4.2 Branching Programs	66	(3)
4.4.3 Read-Once Branching Programs	69	(1)
4.4.4 Complexity of Basic Operations	70	(5)
4.5 References	75	(2)
5. Requirements on Data Structures in Formal Circuit Verification	77	(12)
5.1 Circuit Verification	79	(2)
5.2 Formal Verification of Combinational Circuits	81	(3)
5.3 Formal Verification of Sequential Circuits	84	(2)
5.4 References	86	(3)
Part II. OBDDs: An Efficient Data Structure	89	(84)
6. OBBDDs -- Ordered Binary Decision Diagrams	89	(16)
6.1 Notation and Examples	89	(3)
6.2 Reduced OBDDs: A Canonical Representation of Switching Functions	92	(4)
6.3 The Reduction Algorithm	96	(2)
6.4 Basic Constructions	98	(2)
6.5 Performing Binary Operations and the Equivalence Test	100	(3)
6.6 References	103	(2)
7. Efficient Implementation of OBDDs	105	(18)
7.1 Key Ideas	105	(14)
7.1.1 Shared OBDDs	106	(1)
7.1.2 Unique Table and Strong Canonicity	107	(1)
7.1.3 ITE Algorithm and Computed Table	108	(4)
7.1.4 Complemented Edges	112	(3)
7.1.5 Standard Triples	115	(2)
7.1.6 Memory Management	117	(2)
7.2 Some Popular OBDD Packages	119	(3)
7.2.1 The OBDD Package of Brace, Rudell, and Bryant	119	(1)
7.2.2 The OBDD Package of Long	120	(1)
7.2.3 The CUDD Package: Colorado University Decision Diagrams	120	(2)
7.3 References	122	(1)
8. Influence of the Variable Order on the Complexity of OBDDs	123	(22)
8.1 Connection Between Variable Order and OBDD Size	123	(4)
8.2 Exponential Lower Bounds	127	(8)
8.3 OBDDs with Different Variable Orders	135	(4)
8.4 Complexity of Minimization	139	(5)
8.5 References	144	(1)
9. Optimizing the Variable Order	145	(28)
9.1 Heuristics for Constructing Good Variable Orders	145	(4)
9.1.1 The Fan-In Heuristic	146	(1)
9.1.2 The Weight Heuristic	147	(2)
9.2 Dynamic Reordering	149	(17)
9.2.1 The Variable Swap	151	(4)
9.2.2 Exact Minimization	155	(3)
9.2.3 Window Permutations	158	(1)
9.2.4 The Sifting Algorithm	159	(4)
9.2.5 Block Sifting and Symmetric Sifting	163	(3)
9.3 Quantitative Statements	166	(3)
9.4 Outlook	169	(1)
9.5 References	170	(3)
Part III. Applications and Extensions	173	(84)
10. Analysis of Sequential Systems	173	(26)
10.1 Formal Verification	174	(1)
10.2 Basic Operators	175	(9)
10.2.1 Generalized Cofactors	175	(3)
10.2.2 The Constrain Operator	178	(3)
10.2.3 Quantification	181	(2)
10.2.4 The Restrict Operator	183	(1)
10.3 Reachability Analysis	184	(2)
10.4 Efficient Image Computation	186	(11)
10.4.1 Input Splitting	187	(3)
10.4.2 Output Splitting	190	(1)
10.4.3 The Transition Relation	191	(4)
10.4.4 Partitioning the Transition Relation	195	(2)
10.5 References	197	(2)
11. Symbolic Model Checking	199	(12)
11.1 Computation Tree Logic	199	(3)
11.2 CTL Model Checking	202	(4)
11.3 Implementations	206	(3)
11.3.1 The SMV System	207	(1)
11.3.2 The VIS System	208	(1)
11.4 References	209	(2)
12. Variants and Extensions of OBDDs	211	(24)
12.1 Relaxing the Ordering Restriction	211	(8)
12.2 Alternative Decomposition Types	219	(4)
12.3 Zero-Suppressed BDDs	223	(5)
12.4 Multiple-Valued Functions	228	(5)
12.4.1 Additional Sinks	228	(1)
12.4.2 Edge Values	229	(1)
12.4.3 Moment Decompositions	230	(3)
12.5 References	233	(2)
13. Transformation Techniques for Optimization	235	(22)
13.1 Transformed OBDDs	235	(4)
13.2 Type-Based Transformations	239	(4)
13.2.1 Definition	239	(2)
13.2.2 Circuit Verification	241	(2)
13.3 Linear Transformations	243	(7)
13.3.1 Definition	243	(2)
13.3.2 Efficient Implementation	245	(2)
13.3.3 Linear Sifting	247	(3)
13.4 Encoding Transformations	250	(5)
13.5 References	255	(2)
Bibliography	257	(6)
Index	263