Advanced Techniques in Logic Synthesis, Optimizations and Applications

✍ Scribed by Khatri, Sunil P(Editor);Gulati, Kanupriya(Editor)

• Publisher: Springer New York
• Year: 2010;2011
• Tongue: English
• Leaves: 422
• Edition: 1st ed. 2011
• Category: Library

✦ Synopsis

This book covers recent advances in the field of logic synthesis and design, including Boolean Matching, Logic Decomposition, Boolean satisfiability, Advanced Synthesis Techniques and Applications of Logic Design. All of these topics are valuable to CAD engineers working in Logic Design, Logic Optimization, and Verification. Engineers seeking opportunities for optimizing VLSI integrated circuits will find this book as an invaluable reference, since there is no existing book that covers this material in a systematic fashion.

✦ Table of Contents

20.3.1 Standing Wave Oscillator......Page 5
21.2.4.1 LClkRx < TLClkRx......Page 7
19.6.1 Soft Error Rate (SER) Estimation Using BDEC......Page 19
Cover......Page 1
21.2.2 Clock Acknowledge Latency......Page 3
21.3.1 Optimized Local Clock Generator......Page 9
21.3.2.2 Optimized Input Port Controller......Page 11
20.4.2 Gate Optimization......Page 13
References......Page 16
Contributors......Page 20
21.2.3.1 Demand-Output (D-OUT) Port to Poll-Input (P-IN) Port Channel......Page 4
Preface......Page 6
Contents......Page 8
21.3.2.1 Double Latching Mechanism......Page 10
21.4.1 Input Wrapper Simulation......Page 12
17.5.1.4 Quantification Scheduling......Page 14
21.5 Conclusions......Page 15
21.2.1 Local Clock Generators......Page 2
References......Page 18
20.5 Conclusions......Page 17
19.7 Conclusions......Page 21
References......Page 22
Part I Logic Decomposition......Page 23
2.1 Introduction......Page 24
References......Page 25
2.2 Decomposition Methods......Page 26
2.3 P-Circuits......Page 32
2.3.1 Synthesis Algorithms......Page 34
2.4 Multivariable Decomposition......Page 36
2.5 Experimental Results......Page 39
References......Page 43
3.1 Introduction and Motivation......Page 45
3.2.1 ``Less-Than-or-Equal'' Relation......Page 47
3.2.2 Parameterized Abstraction......Page 48
3.3.1 OR Decomposition......Page 49
3.3.2 XOR Decomposition......Page 50
3.4.1 OR Parameterization......Page 51
3.4.2 XOR Parameterization......Page 52
3.5.1 Extraction of Incompletely Specified Logic......Page 53
3.5.2 Exploring Decomposition Choices......Page 54
3.5.3 Synthesis Algorithm......Page 55
3.6 Experimental Evaluation......Page 56
3.7 Conclusions and Future Work......Page 58
References......Page 59
4.1 Introduction......Page 60
4.2 Background......Page 61
4.3 General Non-disjoint Decompositions......Page 63
4.4.1 Global View......Page 66
4.4.2 Cut Computation......Page 67
4.4.3 Cuts with a DSD Structure......Page 69
4.4.5 Decomposition and Network Update......Page 70
4.4.6 Finding the Maximum Support-ReducingDecomposition......Page 71
4.4.7.2 Restricting Bound Sets for Balanced Decompositions......Page 73
4.5 Comparison with Boolean Matching......Page 74
4.6 Experimental Results......Page 75
4.7 Conclusions and Future Work......Page 77
References......Page 78
5.1 Introduction......Page 80
5.2 Previous Work......Page 82
5.3.1 Functional Decomposition......Page 83
5.3.3.1 Refutation Proof and Craig Interpolation......Page 84
5.3.3.2 Circuit-to-CNF Conversion......Page 85
5.4.1.2 Decomposition with Unknown Variable Partition......Page 88
5.4.2 Multiple-Output Ashenhurst Decomposition......Page 92
5.4.3 Beyond Ashenhurst Decomposition......Page 93
5.6 Chapter Summary......Page 97
6.1 Introduction......Page 99
6.2 Previous Work......Page 100
6.3.1 Bi-Decomposition......Page 101
6.3.2.1 Refutation Proof and Craig Interpolation......Page 102
6.4.1.1 Decomposition of Completely Specified Functions......Page 103
6.4.1.2 Decomposition of Incompletely Specified Functions......Page 109
6.4.3.1 Decomposition of Completely Specified Functions......Page 110
6.4.4 Implementation Issues......Page 113
6.6 Summary......Page 115
References......Page 116
Part II Boolean Satisfiability......Page 118
7.1 Introduction......Page 119
7.2 Basic Definitions......Page 121
7.3.1 Basic Propositions......Page 122
7.3.2 Elimination of Boundary Points by Adding Resolvents......Page 123
7.3.3 Boundary Points and Redundant Formulas......Page 125
7.4.1 Resolution Proof as Boundary Point Elimination......Page 126
7.5 Equivalence Checking Formulas......Page 127
7.5.1 Building Equivalence Checking Formulas......Page 128
7.5.2 Short Proofs for Equivalence Checking Formulas......Page 129
7.6 Experimental Results......Page 130
7.7 Some Background......Page 132
7.8.1 Cut Boundary Points......Page 133
7.8.2 The Completeness Result......Page 134
7.8.3 Boundary Points as Complexity Measure......Page 135
7.9 Conclusions and Directions for Future Research......Page 136
8.1 Introduction......Page 138
8.2 Previous Work......Page 139
8.3.1 And-Inverter Graphs......Page 140
8.3.2 SAT Sweeping......Page 141
8.4.2 Observability Don't Cares......Page 143
8.4.3 Algorithm......Page 146
8.4.4 Implementation......Page 148
8.4.5 Applications......Page 150
8.5 Results......Page 151
8.6 Conclusions......Page 155
References......Page 156
9.1 Introduction......Page 158
9.2 Preliminaries......Page 160
9.3.1 RelaxSAT......Page 162
9.3.2 Relaxation Heuristic......Page 164
9.3.3 Discussion on Computation Complexity......Page 165
9.5 Application Discussion: A RelaxSAT-Based MAX-SAT Solver......Page 170
9.5.1 The New MAX-SAT Solver: RMAXSAT......Page 172
9.5.2 Evaluation of MAX-SAT Solver......Page 174
9.6 Conclusions and Future Works......Page 177
References......Page 178
10.1 Introduction......Page 180
10.2.1 The MaxSAT Problem......Page 181
10.2.2 Solving MaxSAT with PBO......Page 182
10.3 A New MaxSAT Algorithm......Page 183
10.3.1 Overview......Page 184
10.3.3 A Complete Example......Page 185
10.4 Experimental Results......Page 187
10.5 Related Work......Page 189
References......Page 190
Part III Boolean Matching......Page 192
11.1 Introduction......Page 193
11.2.1 Boolean Matching......Page 194
11.2.3 And-Inverter Graph......Page 195
11.3 Detection of Functional Property Using S&S Approach......Page 196
11.4 Definitions and Notations......Page 197
11.5 Simulation Approach for Distinguishing Inputs......Page 198
11.5.1 Type-1......Page 199
11.5.3 Type-3......Page 200
11.6.2 Recursive-Matching Algorithm......Page 202
11.6.3.3 Analysis of Space Complexity and Runtime......Page 204
11.7 Experimental Results......Page 205
11.8 Chapter Summary......Page 208
12.1 Introduction and Background......Page 210
12.2 Previous Work......Page 212
12.3 DeltaSyn......Page 213
12.3.1 Phase I: Equivalence-Based Reduction......Page 214
12.3.2 Phase II: Matching-Based Reduction......Page 216
12.3.2.1 Subcircuit Enumeration......Page 217
12.3.2.2 Subcircuit Matching......Page 220
12.3.2.3 Subcircuit Covering......Page 224
12.3.3 Phase III: Functional Hashing-Based Reduction......Page 225
12.4 Empirical Validation......Page 227
References......Page 231
13.1 Introduction......Page 233
13.2 Background and Previous Work......Page 235
13.2.2 And-Inverter Graphs (AIGs)......Page 236
13.2.3 Boolean Satisfiability and Equivalence Checking......Page 237
13.3.1 Computing I/O Support Variables......Page 238
13.3.2 Initial refinement of I/O clusters......Page 239
13.3.4 Refining I/O by Unateness......Page 240
13.3.6 Scalable I/O Refinement by Random Simulation......Page 241
13.3.6.2 Simulation Type 2......Page 242
13.3.6.3 Simulation Type 3......Page 243
13.4.1 SAT-Based Input Matching......Page 244
13.4.2 Pruning Invalid Input Matches by SATCounterexamples......Page 245
13.4.3 SAT-Based Output Matching......Page 246
13.4.5 Pruning Invalid I/O Matches Using Support Signatures......Page 247
13.4.7 A Heuristic for Matching Candidates......Page 248
References......Page 252
Part IV Logic Optimization......Page 254
14.1 Introduction......Page 255
14.1.1 Motivation......Page 256
14.1.3 Paper Organization......Page 257
14.2.1 Kernel/Co-kernel Extraction......Page 258
14.3.1 Polynomial Functions and Their Canonical Representations......Page 259
14.3.2 Factorization......Page 261
14.4.1 Common Coefficient Extraction......Page 262
14.4.2 Common Cube Extraction......Page 263
14.4.3 Algebraic Division......Page 264
14.5 Integrated Approach......Page 265
14.6 Experiments......Page 268
14.7 Conclusions......Page 269
15.1 Introduction......Page 271
15.2.2 Sets of Pairs of Functions to Be Distinguished......Page 273
15.3 Approximating SPFDs......Page 274
15.3.1 Computing aSPFDs for Combinational Circuits......Page 275
15.3.2 Computing aSPFDs for Sequential Circuits......Page 277
15.3.3 Optimizing aSPFDs with Don't Cares......Page 278
15.3.3.1 Conflicts in Multiple Expected Traces......Page 279
15.4 Logic Transformations with aSPFDs......Page 281
15.4.1 SAT-Based Searching Algorithm......Page 282
15.4.2 Greedy Searching Algorithm......Page 283
15.5.1 Logic Restructuring of Combinational Designs......Page 284
15.5.2 Logic Restructuring of Sequential Designs......Page 287
15.6 Summary......Page 289
16.1 Introduction......Page 291
16.3.1 Boolean Relation......Page 294
16.3.2 Satisfiability and Interpolation......Page 295
16.4.1.1 Total Relation......Page 296
16.4.1.2 Partial Relation......Page 297
16.4.2.1 Determinization via Expansion Reduction......Page 298
16.4.2.2 Determinization via Substitution Reduction......Page 299
16.4.3 Deterministic Relation......Page 300
16.4.4.1 Support Minimization......Page 301
16.4.4.2 Determinization Scheduling......Page 302
16.6 Chapter Summary......Page 309
References......Page 310
17.1 Introduction......Page 312
17.2 Problem Definition......Page 314
17.3 Previous Work......Page 315
17.4 Preliminaries and Definitions......Page 317
17.4.1 BREL Boolean Relation Minimizer......Page 319
17.5 Approach......Page 320
17.5.1.1 Selecting Node Pairs......Page 321
17.5.1.2 Building the Subnetwork......Page 323
17.5.1.3 Computing the Boolean Relation RY......Page 324
17.5.1.4 Quantification Scheduling......Page 325
17.5.1.5 Endgame......Page 327
17.6.2.1 Selecting......Page 328
17.6.2.3 Selecting thresh......Page 330
17.6.3 Comparison of the Proposed Technique with mfsw......Page 331
17.6.4.1 Running relation After mfsw......Page 333
17.6.4.4 Effects of Early Quantification......Page 334
17.7 Chapter Summary......Page 335
References......Page 336
Part V Applications to Specialized Design Scenarios......Page 338
18.1 Introduction and Background......Page 339
18.3.1 Generating Decimal Probabilities from the Input Probability Set S = {0.4, 0.5}......Page 343
18.3.2 Generating Decimal Probabilities from the Input Probability Set S = {0.5, 0.8}......Page 347
18.4 Sets with a Single Element that Can Generate Arbitrary Decimal Probabilities......Page 350
18.5 Implementation......Page 353
18.6 Empirical Validation......Page 357
18.7 Chapter Summary......Page 358
References......Page 359
19.1 Introduction......Page 360
19.2.1 Partial Boolean Difference......Page 362
19.2.2 Total Boolean Difference......Page 363
19.2.3 Signal and Error Probabilities......Page 364
19.3.1 Gate Error Model......Page 365
19.3.2 Error Propagation in 2-to-1 Mux Using BDEC......Page 368
19.3.3 Circuit Error Model......Page 370
19.4.1 Output Error Expression......Page 371
19.4.2 Reconvergent Fanout......Page 372
19.5 Simulation Results......Page 374
19.6.1 Soft Error Rate (SER) Estimation Using BDEC......Page 378
19.6.3 BDEC Applied to Emerging Nanotechnologies......Page 380
References......Page 381
20.1 Introduction......Page 383
20.2 Previous Work......Page 386
20.3.1 Standing Wave Oscillator......Page 387
20.3.2.1 Multiplier......Page 389
20.3.2.2 Low-Pass Filter......Page 391
20.3.2.4 Complex Gates......Page 392
20.4.1 Sinusoid Generator......Page 393
20.4.2 Gate Optimization......Page 395
20.4.3 Gate Operation......Page 397
20.5 Conclusions......Page 399
References......Page 400
Subject Index......Page 401
21.1 Introduction......Page 406
21.2.1 Local Clock Generators......Page 407
21.2.2 Clock Acknowledge Latency......Page 408
21.2.3.1 Demand-Output (D-OUT) Port to Poll-Input (P-IN) Port Channel......Page 409
21.2.3.2 Other Point-to-Point Channels......Page 411
21.2.4.1 LClkRx < TLClkRx......Page 412
21.2.4.2 LClkRx TLClkRx......Page 413
21.3.1 Optimized Local Clock Generator......Page 414
21.3.2.1 Double Latching Mechanism......Page 415
21.3.2.2 Optimized Input Port Controller......Page 416
21.4.1 Input Wrapper Simulation......Page 417
21.4.2 Point-to-Point Communication......Page 420
References......Page 421