A Circuit-Based Boolean Solver and Its Application to Rewiring-Based Logic Optimization

在本論文中，我們提出了一個以滿足性解法為基礎的邏輯最佳化平台，它包含了在電路上建全的布林滿足性解法器、強力的多餘連線之移除及加入工具、和虛擬布林最佳器，它可以被用來做超大規模積體電路的驗證和邏輯最佳化。這個滿足性解法器是被實行在縮減函式的邏輯閘「且-反向」圖形之結構上，因此它在半標準型態的電路上有比較強的蘊涵能力。此外，我們提昇了這個圖形表示法讓它記錄更多邏輯蘊涵和允許多輸入的閘，且不同於其他人的滿足性解法器是透過合取範式為基礎，我們直接在此電路圖形上實踐滿足性解法器以獲得完全的結構資訊。而且我們綜合了滿足性解法中的變數決定法，和多餘連線之移除及加入演算法，使其更有的彈性和效率。最後，我們將滿足性解法器延伸到虛擬布林最佳化引擎，並創造了多重的多餘連線之移除及加入技術。我們應用此技術到電路最佳化問題上，實驗數據顯示出我們的架構相對於原本的方法有重大的改善。In this thesis, we proposed a SAT-based logic optimization framework which contains a robust Boolean satisfiability (SAT) solver, a powerful redundancy-addition-and- removal (RAR) engine, and a Pseudo-Boolean optimizer on the circuit netlist. It can be used for the verification and logic optimization of the VLSI circuits. The SAT solver is implemented on the FRAIG (Functionally Reduced And-Inverter Graph) structure so that it has stronger implicability on a semi-canonical circuit netlist. We further revised the FRAIG by recording more logic implications and allowing multi-input gates. Different from other FRAIG packages where the SAT engine is based on a separated Conjunctive-Normal-Form (CNF) based solver, we implemented the SAT algorithms directly on FRAIG so that the structural information can be fully utilized. Moreover, we incorporated the SAT decision making and RAR techniques so that the RAR-based logic optimization can be more flexible and efficient. Lastly, we extended our SAT solver to a Pseudo Boolean (PB) optimizer and proposed a multiple RAR technique. We applied these techniques for circuit optimization and the experimental results show that our framework can achieve significant improvement over the traditional approaches.誌謝 I要 IIbstract IIIable of Contents IVist of Figures VIIIist of Tables IXhapter 1 Introduction 1.1 Boolean Satisfiability 2.2 Functionally Reduced And-Inverter Graph (FRAIG) 3.3 Pseudo Boolean Optimization Problem 4.4 Redundancy Addition and Removal 5.5 Thesis Contributions 6hapter 2 Preliminaries and Background 7.1 Key Techniques in SAT Algorithms 7.1.1 DPLL Algorithm 7.1.2 Boolean Constraint Propagation (BCP) 8.1.3 Conflict Analysis 9.1.4 Decision Strategies 11.1.5 Translate the Circuit to CNF 12.2 FRAIG Circuit Representation 12.2.1 Structure Hashing 12.2.2 Random Simulation 13.2.3 Functional Equivalence Checking by SAT 13.2.4 Counterexample-Enhanced Simulation 13.2.5 Equivalence Class 14.3 PB Optimization Solver 15.3.1 Normalization of PB Constraints 15.3.2 Translation from PB-Constraints into CNF 16.3.3 Integrating PB-constraints into the SAT Solver 17.3.4 PB Optimization Procedure 18.4 RAR Techniques 18.4.1 Mandatory Assignment and Redundancy Check 19.4.2 The Algorithm of RAMBO 19.4.3 The Algorithm of Two-way RAR 21hapter 3 Circuit-Based Boolean Solver 23.1 Circuit-Based SAT Solver 23.1.1 Logic Implications in the Circuit 23.1.2 Decision Heuristics 25.1.3 Conflict-Driven Learning 25.2 FRAIG Enhancement 26.2.1 Multi-input AIG 26.2.2 Functional Equivalence Checking by Simulation and SAT 27.2.3 Enhancing Simulation Data by Intersection of Counterexample 27.2.4 Maintaining Original Logic Implication for Removed Gate 28.2.5 Experimental Results 29.3 Implementation of Pseudo Boolean Solver 31.3.1 Translating Pseudo Boolean Constraints into AND-OR Circuit 31.3.2 Translating Pseudo Boolean Constraints into Adders 34.3.3 PB Optimization Procedure 36.3.4 Experimental Results 37hapter 4 Application to Logic Optimization by Multiple RAR 39.1 SAT-Controlled RAR 39.1.1 Removal and Addition of Wires 39.1.2 Theorems for SAT-Controlled RAR 41.1.3 Implication Graph Filter 43.1.4 Experimental Results 44.2 Logic Optimization by Multiple RAR 47.2.1 Algorithm Overview 47.2.2 Modeling of Multiple RAR 47.2.3 Level Optimization Algorithm 49.2.4 The Method of Blocking Solution 50.2.5 Experimental Results 51hapter 5 Conclusions and Future Work 54eference 5