search for books and compare prices
Tables of Contents for Algorithms and Data Structures in Vlsi Design
Chapter/Section Title
Page #
Page Count
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