請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/37725
完整後設資料紀錄
DC 欄位 | 值 | 語言 |
---|---|---|
dc.contributor.advisor | 黃鐘揚(Chung-Yang Huang) | |
dc.contributor.author | Chi-An Wu | en |
dc.contributor.author | 吳濟安 | zh_TW |
dc.date.accessioned | 2021-06-13T15:40:34Z | - |
dc.date.available | 2008-07-21 | |
dc.date.copyright | 2008-07-21 | |
dc.date.issued | 2008 | |
dc.date.submitted | 2008-07-07 | |
dc.identifier.citation | [1] Ellen M. Sentovich, Kanwar Jit Singh, Luciano Lavagno, Cho Moon, Rajeev Murgai. Alexander Saldanha, Hamid Savoj, Paul R. Stephan, Robert K. Brayton, Alberto Sangiovanni-Vincentelli, “SIS: A System for Sequential Circuit Synthesis”, Department of Electrical Engineering and Computer Science, University of California, Berkeley, CA, May 1992
[2] R. Alur, T. Henzinger, and New Brunswick, NJ, “VIS: A system for Verification and Synthesis”, in Proceedings of the 8th International Conference on Computer Aided Verification, pp. 428-432, July 1996, http://vlsi.colorado.edu/~vis/ [3] MVSIS: Logic Synthesis and Verification, http://embedded.eecs.berkeley.edu/Respep/Research/mvsis/index.html [4] ABC: A System for Sequential and Verification, http://www.eecs.berkeley.edu/~alanmi/abc/ [5] M.W. Moskewicz, C.F. Madigan, Y. Zhao, L. Zhang, and S. Malik “Chaff: Engineering an Efficient SAT Solver”, in Proceedings of Design Automation Conference, June 2001 [6] S. A. Cook, “The Complexity of Theorem Proving Procedures”, in Proceedings of the third Annual ACM Symposium on the Theory of Computing, pp. 151-158, 1971 [7] R. E. Bryant, “Graph-based Algorithms for Boolean Function Manipulation”, IEEE Transactions on Computers, Vol. C-35, No. 8, pp. 677-691, August, 1986 [8] K. S. Brace, R. L. Rudell, and R. E. Bryant. “Efficient Implementation of a BDD Package”, Design Automation Conference, 1990 [9] F. Somenzi, “CUDD: CU Decision Diagram Package”, http://vlsi.colorado.edu/~fabio/CUDD/cuddIntro.html [10] Niklas Een and Niklas Sörensson, “An Extensible SAT-Solver SAT”, in Proceedings of the 6th International Conference on Theory and Applications of Satisability Testing, 2003, http://minisat.se/MiniSat.html [11] Knot Pipatsrisawat and Adnan Darwiche, “RSat 2.0: SAT Solver Description”, SAT Competition 2007, http://reasoning.cs.ucla.edu/rsat/ [12] Alan Mishchenko, Satrajit Chatterjee, Roland Jiang, and Robert K. Brayton, “FRAIGs: A Unifying Representation for Logic Synthesis and Verification”, ERL Technical Report, EECS Dept., UC Berkeley, March 2005 [13] Alan Mishchenko, Satrajit Chatterjee, Robert Brayton, and Niklas Een, “Improvements to Combinational Equivalence Checking”, in Proceddings of International Conference on Computer-Aided Design, 2006 [14] F. Pigorsch, C. Scholl, and S. Disch, “Advanced Unbounded CTL Model Checking By Using AIGs, BDD Sweeping, And Quantifier Scheduling”, in Proceedings of Formal Methods in Computer-Aided Design, 2006 [15] Niklas Een and Niklas Sörensson, “Translating Pseudo-Boolean Constraints into SAT”, Journal on Satisfiability, Boolean Modeling and Computation, 2006 [16] Hossein M. Sheini and Karem A. Sakallah, “Pueblo: A Hybrid Pseudo-Boolean SAT Solver”, Journal on Satisfiability, Boolean Modeling and Computation, issue 2, pp. 157–181, 2006 [17] Chih-Wei Jim Chang, Ming-Fu Hsiao, and Malgorzata Marek-Sadowska, “A New Reasoning Scheme for Efficient Redundancy Addition and Removal”, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 22, pp. 945-951 , 2003 [18] Luis A. Entrena and Kwang-Ting Cheng: “Combinational and Sequential Logic Optimization by Redundancy Addition and Removal”, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 14, pp. 909-916, 1995 [19] Luis A. Entrena, Jos A. Espejo, Emilio Olas, and Javier Uceda, “Timing Optimization by an Improved Redundancy Addition and Removal Technique”, in Proceedings of the Conference on European Design Automation, 1996 [20] Shih-Chieh Chang, Malgorzata Marek-Sadowska, and Kwang-Ting Cheng, “Perturb and Simplify: Multilevel Boolean Network Optimizer”, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 15(12), pp. 1494-1504, 1996 [21] Mahesh A. Iyer and Miron Abramovici, “FIRE: A Fault-Independent Combinational Redundancy Identification Algorithm”, IEEE Transactions on Very Large Scale Integration Systems 4, 2, pp. 295-301, 1996 [22] M. Davis and H. Putnam, “A Computing Procedure for Quantification Theory', Journal of the ACM, Vol. 7, pp. 201-214, 1960 [23] M. Davis, G. Logemann, and D. Loveland, “A Machine Program for Theorem -Proving”, Communications of ACM, Vol. 5, No. 7, pp. 394-397, 1962 [24] H. Zhang, “SATO: An Efficient Propositional Prover” , in Proceedings of the International Conference on Automated Deduction, pp. 272-275, July 1997 [25] Marques-Silva, J. P., and Sakallah, K. A., “GRASP: A Search Algorithm for Propositional Satisfiability”, IEEE Transactions on Computers, Vol. 48, pp. 506-521, 1999 [26] Niklas Een and Niklas Sörensson, “MiniSat v1.13 – A SAT Solver with Conflict- Clause Minimization”, SAT Competition 2005 [27] E. Goldberg and Y. Novikov, “Berkmin: A Fast and Robust SAT-Solver”, in Proceedings of Design, Automation and Test in Europe Conference, 2002 [28] Henry Kautz, Eric Horvitz, Yongshao Ruan, Carla Gomes, and Bart Selman, “Dynamic Restart Policies”, the Eighteenth National Conference on Artificial Intelligence, 2002 [29] G. Tseitin, “On the Complexity of Derivation in Propositional Calculus”, Studies in Constructive Mathematics and Mathematical Logic, 1968 [30] D. Chai and A. Kuehlmann, “A Fast Pseudo-Boolean Constraint Solver”, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 24(3), pp. 305–317,2005 [31] Bailleux, Y. Boufkhad, and O. Roussel., “A Translation of Pseudo Boolean Constraints to SAT”, Journal on Satisfiability, Boolean Modeling and Computation , issue 2, pp. 183–192, 2006 [32] L. Dadda , “Some Schemes for Parallel Multipliers” , Alta Frequenza, Volume 34, pp. 14–17, 1964 [33] Chi-An Wu, Ting-Hao Lin, Chih-Chun Lee and Chung-Yang (Ric) Huang, “QuteSAT: A Robust Circuit-based SAT Solver for Complex Circuit Structure”, in Proceedings of the Conference on Design, Automation and Test in Europe 2007 [34] ITC’99 benchmarks, http://www.cad.polito.it/tools/itc99.html [35] Miroslav Velev’s SAT Benchmarks, http://www.miroslav-velev.com/sat_benchmarks.html | |
dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/37725 | - |
dc.description.abstract | 在本論文中,我們提出了一個以滿足性解法為基礎的邏輯最佳化平台,它包含了在電路上建全的布林滿足性解法器、強力的多餘連線之移除及加入工具、和虛擬布林最佳器,它可以被用來做超大規模積體電路的驗證和邏輯最佳化。這個滿足性解法器是被實行在縮減函式的邏輯閘「且-反向」圖形之結構上,因此它在半標準型態的電路上有比較強的蘊涵能力。此外,我們提昇了這個圖形表示法讓它記錄更多邏輯蘊涵和允許多輸入的閘,且不同於其他人的滿足性解法器是透過合取範式為基礎,我們直接在此電路圖形上實踐滿足性解法器以獲得完全的結構資訊。而且我們綜合了滿足性解法中的變數決定法,和多餘連線之移除及加入演算法,使其更有的彈性和效率。最後,我們將滿足性解法器延伸到虛擬布林最佳化引擎,並創造了多重的多餘連線之移除及加入技術。我們應用此技術到電路最佳化問題上,實驗數據顯示出我們的架構相對於原本的方法有重大的改善。 | zh_TW |
dc.description.abstract | 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. | en |
dc.description.provenance | Made available in DSpace on 2021-06-13T15:40:34Z (GMT). No. of bitstreams: 1 ntu-97-R95921028-1.pdf: 431270 bytes, checksum: 955b42a0a16f6426ccf761be1d0bfddc (MD5) Previous issue date: 2008 | en |
dc.description.tableofcontents | 誌謝 I
摘要 II Abstract III Table of Contents IV List of Figures VIII List of Tables IX Chapter 1 Introduction 1 1.1 Boolean Satisfiability 2 1.2 Functionally Reduced And-Inverter Graph (FRAIG) 3 1.3 Pseudo Boolean Optimization Problem 4 1.4 Redundancy Addition and Removal 5 1.5 Thesis Contributions 6 Chapter 2 Preliminaries and Background 7 2.1 Key Techniques in SAT Algorithms 7 2.1.1 DPLL Algorithm 7 2.1.2 Boolean Constraint Propagation (BCP) 8 2.1.3 Conflict Analysis 9 2.1.4 Decision Strategies 11 2.1.5 Translate the Circuit to CNF 12 2.2 FRAIG Circuit Representation 12 2.2.1 Structure Hashing 12 2.2.2 Random Simulation 13 2.2.3 Functional Equivalence Checking by SAT 13 2.2.4 Counterexample-Enhanced Simulation 13 2.2.5 Equivalence Class 14 2.3 PB Optimization Solver 15 2.3.1 Normalization of PB Constraints 15 2.3.2 Translation from PB-Constraints into CNF 16 2.3.3 Integrating PB-constraints into the SAT Solver 17 2.3.4 PB Optimization Procedure 18 2.4 RAR Techniques 18 2.4.1 Mandatory Assignment and Redundancy Check 19 2.4.2 The Algorithm of RAMBO 19 2.4.3 The Algorithm of Two-way RAR 21 Chapter 3 Circuit-Based Boolean Solver 23 3.1 Circuit-Based SAT Solver 23 3.1.1 Logic Implications in the Circuit 23 3.1.2 Decision Heuristics 25 3.1.3 Conflict-Driven Learning 25 3.2 FRAIG Enhancement 26 3.2.1 Multi-input AIG 26 3.2.2 Functional Equivalence Checking by Simulation and SAT 27 3.2.3 Enhancing Simulation Data by Intersection of Counterexample 27 3.2.4 Maintaining Original Logic Implication for Removed Gate 28 3.2.5 Experimental Results 29 3.3 Implementation of Pseudo Boolean Solver 31 3.3.1 Translating Pseudo Boolean Constraints into AND-OR Circuit 31 3.3.2 Translating Pseudo Boolean Constraints into Adders 34 3.3.3 PB Optimization Procedure 36 3.3.4 Experimental Results 37 Chapter 4 Application to Logic Optimization by Multiple RAR 39 4.1 SAT-Controlled RAR 39 4.1.1 Removal and Addition of Wires 39 4.1.2 Theorems for SAT-Controlled RAR 41 4.1.3 Implication Graph Filter 43 4.1.4 Experimental Results 44 4.2 Logic Optimization by Multiple RAR 47 4.2.1 Algorithm Overview 47 4.2.2 Modeling of Multiple RAR 47 4.2.3 Level Optimization Algorithm 49 4.2.4 The Method of Blocking Solution 50 4.2.5 Experimental Results 51 Chapter 5 Conclusions and Future Work 54 Reference 55 | |
dc.language.iso | en | |
dc.title | 在電路上實現之布林函數解法器以及它在利用電路重新連線進行邏輯最佳化之應用 | zh_TW |
dc.title | A Circuit-Based Boolean Solver and Its Application to Rewiring-Based Logic Optimization | en |
dc.type | Thesis | |
dc.date.schoolyear | 96-2 | |
dc.description.degree | 碩士 | |
dc.contributor.oralexamcommittee | 江介宏(Jie-Hong Jiang),李建模(Chien-Mo Li) | |
dc.subject.keyword | 滿足性問題,縮減函式的邏輯閘且反向圖形,虛擬布林,多餘連線之移除及加入,邏輯合成,最佳化與驗證, | zh_TW |
dc.subject.keyword | Boolean Satisfiability (SAT),functionally reduced AND-INV graph (FRAIG),pseudo Boolean (PB),redundancy addition and removal (RAR),logic synthesis,optimization and verification, | en |
dc.relation.page | 58 | |
dc.rights.note | 有償授權 | |
dc.date.accepted | 2008-07-08 | |
dc.contributor.author-college | 電機資訊學院 | zh_TW |
dc.contributor.author-dept | 電機工程學研究所 | zh_TW |
顯示於系所單位: | 電機工程學系 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
ntu-97-1.pdf 目前未授權公開取用 | 421.16 kB | Adobe PDF |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。