Advanced Techniques in Logic Synthesis, Optimizations and Applications

Advanced Techniques in Logic Synthesis, Optimizations and Applications Edited by: Sunil P Khatri Kanupriya Gulati 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. •Covers the latest research in the areas of Boolean Matching, Logic Decomposition, Boolean Satisfiability •Serves as a single-source reference to key topics in logic synthesis, otherwise only available in disparate publications; •Describes a range of synthesis techniques and Applications of logic design 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