請用此 Handle URI 來引用此文件：
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/3826完整後設資料紀錄
| DC 欄位 | 值 | 語言 |
|---|---|---|
| dc.contributor.advisor | 黃鐘揚(Chung-Yang (Ric) | |
| dc.contributor.author | Li-Wei Wang | en |
| dc.contributor.author | 王立為 | zh_TW |
| dc.date.accessioned | 2021-05-13T08:37:13Z | - |
| dc.date.available | 2016-08-24 | |
| dc.date.available | 2021-05-13T08:37:13Z | - |
| dc.date.copyright | 2016-08-24 | |
| dc.date.issued | 2016 | |
| dc.date.submitted | 2016-08-01 | |
| dc.identifier.citation | [1] Robert K Brayton, Richard Rudell, Alberto Sangiovanni-Vincentelli, and Albert R Wang, “Mis: A multiple-level logic optimization system,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 6, no. 6, pp. 1062–1081, 1987.
[2] Robert Brayton and Alan Mishchenko, “Abc: An academic industrial-strength verification tool,” in International Conference on Computer Aided Verification. Springer, 2010, pp. 24–40. [3] Luca Amar´u, Pierre-Emmanuel Gaillardon, and Giovanni De Micheli, “Majority-inverter graph: A novel data-structure and algorithms for efficient logic optimization,” in Proceedings of the 51st Annual Design Automation Conference. ACM, 2014, pp. 1–6. [4] Luca Amar´u, Pierre-Emmanuel Gaillardon, and Giovanni De Micheli, “Boolean logic optimization in majority-inverter graphs,” in 2015 52nd ACM/EDAC/IEEE Design Automation Conference (DAC). IEEE, 2015, pp. 1–6. [5] Per Bjesse and Arne Boralv, “Dag-aware circuit compression for formal verification,” in Proceedings of the 2004 IEEE/ACM International conference on Computeraided design. IEEE Computer Society, 2004, pp. 42–49. [6] Alan Mishchenko, Satrajit Chatterjee, and Robert Brayton, “Dag-aware aig rewriting a fresh look at combinational logic synthesis,” in Proceedings of the 43rd annual Design Automation Conference. ACM, 2006, pp. 532–535. [7] Vin´ıcius P Correia and Andr´e I Reis, “Classifying n-input boolean functions,” in VII Workshop Iberchip, 2001, p. 58. [8] Daniel Brand, “Verification of large synthesized designs,” in The Best of ICCAD, pp. 65–72. Springer, 2003. [9] Andreas Kuehlmann, Viresh Paruthi, Florian Krohm, and Malay K Ganai, “Robust boolean reasoning for equivalence checking and functional property verification,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 21, no. 12, pp. 1377–1394, 2002. [10] Alan Mishchenko, Satrajit Chatterjee, Robert Brayton, and Niklas Een, “Improvements to combinational equivalence checking,” in 2006 IEEE/ACM International Conference on Computer Aided Design. IEEE, 2006, pp. 836–843. [11] Randal E Bryant, “Graph-based algorithms for boolean function manipulation,” IEEE Transactions on computers, vol. 100, no. 8, pp. 677–691, 1986. [12] Niklas Sorensson and Niklas Een, “Minisat v1. 13-a sat solver with conflict-clause minimization,” SAT, vol. 2005, pp. 53, 2005. [13] Jiang Long, Robert K Brayton, and Michael Case, “Lec: Learning driven data-path equivalence checking,” Prof. of DIFTS@ FMCAD, pp. 9–18, 2013. [14] Grigori S Tseitin, “On the complexity of derivation in propositional calculus,” in Automation of reasoning, pp. 466–483. Springer, 1983. [15] Demosthenes Anastasakis, Lisa McIlwain, and Slawomir Pilarski, “Efficient equivalence checking with partitions and hierarchical cut-points,” in Proceedings of the 41st annual Design Automation Conference. ACM, 2004, pp. 539–542. [16] Alan Mishchenko, Satrajit Chatterjee, Roland Jiang, and Robert K Brayton, “Fraigs: A unifying representation for logic synthesis and verification,” Tech. Rep., ERL Technical Report, 2005. [17] Maciej Ciesielski, Cunxi Yu, Walter Brown, Duo Liu, and Andr´e Rossi, “Verification of gate-level arithmetic circuits by function extraction,” in Proceedings of the 52nd Annual Design Automation Conference. ACM, 2015, p. 52. [18] Valeria Bertacco and Maurizio Damiani, “The disjunctive decomposition of logic functions,” in Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design. IEEE Computer Society, 1997, pp. 78–82. [19] Mathias Soeken, Luca Gaetano Amar, Pierre-Emmanuel Gaillardon, and Giovanni De Micheli, “Optimizing majority-inverter graphs with functional hashing,” in 2016 Design, Automation&Test in Europe Conference&Exhibition (DATE). IEEE, 2016, pp. 1030–1035. [20] Leonardo De Moura and Nikolaj Bj?rner, “Z3: An efficient smt solver,” in Internationalnconference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2008, pp. 337–340. | |
| dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/3826 | - |
| dc.description.abstract | 眾數反向圖是近年來提出的一種邏輯電路表示法，他將邏輯電路用眾數函數與反向函數組合而成；他的代數與布林特性讓他在邏輯優化的操作上非常有效率，比起目前最先進的方法，眾數反向圖的演算法可以得到更佳的結果。在這篇論文中，我們將無圈有向改寫技術鑲嵌進眾數反向圖，並將其應用在邏輯合成與驗證領域。在邏輯合成方面，實驗結果顯示高度優化的眾數反向圖仍可被我們的演算法再優化；在資料路徑驗證方面，我們的演算法可以提高資料路徑分析的品質，並有效的減少正規驗證所需的時間。 | zh_TW |
| dc.description.abstract | A Majority-Inverter Graph (MIG) is a recently introduced logic representation form which manipulates logic by using only 3-input majority function (MAJ) and inversion function (INV). Its algebraic and Boolean properties enables efficient logic optimizations. In particular, MIG algorithms obtained significantly superior synthesis results as compared to the state-of-the-art approaches based on AND-inverter graphs and commercial tools. In this thesis, we integrate the DAG-aware rewriting technique, a fast greedy algorithm for circuit compression, into MIG and apply it not only in the logic synthesis but also verification. Experimental results on logic optimization show that heavily-optimized MIGs can be further reduced by 20.4% of network size while depth preserved. Experimental results on datapath verification also show the effectiveness of our algorithm. With our MIG rewriting applied, datapath analysis quality can be improved with the ratio 3.16. Runtime for equivalence checking can also be effectively reduced. | en |
| dc.description.provenance | Made available in DSpace on 2021-05-13T08:37:13Z (GMT). No. of bitstreams: 1 ntu-105-R03943084-1.pdf: 1582033 bytes, checksum: 8a24cb3fa5b9251e6330e17de258f5e7 (MD5) Previous issue date: 2016 | en |
| dc.description.tableofcontents | Chapter 1 Introduction 1
Chapter 2 Preliminaries 3 2.1 Function Classification 3 2.1.1 The Concept of P Class 3 2.1.2 The Concept of NPN Class 3 2.2 Formal Verification 4 2.2.1 Combinational Equivalence Checking 5 2.2.2 Datapath Analysis 7 2.3 Previous Work on Majority-Inverter Graph 10 2.3.1 MIG Logic Representation 11 2.3.2 MIG Boolean Algebra 12 2.3.3 Logic Optimization Using Algebraic Transformation 14 2.3.4 MIG Boolean Methods and Logic Optimization 16 Chapter 3 DAG-Aware MIG Rewriting 20 3.1 An Overwiew of Our Framework 20 3.2 Subgraph Preparation Phase 21 3.2.1 Exact Synthesis 21 3.2.2 Subgraph Generation 26 3.2.3 Subgraph Storage 28 3.3 Rewriting Phase 30 3.3.1 Subgraph Loading 30 3.3.2 Subgraph NPN Manipulation 31 Chapter 4 Application of DAG-Aware MIG Rewriting 33 4.1 From the Perspective of Logic Synthesis 33 4.1.1 Rewriting Methodology for Logic Optimization 33 4.1.2 A Demonstration Example 34 4.2 From the Perspective of Datapath Verification 36 4.2.1 Motivation 36 4.2.2 Datapath Normalization 38 Chapter 5 Experimental Results 41 5.1 Logic Synthesis Results 41 5.1.1 Methodology 41 5.1.2 Optimization Results 42 5.2 Datapath Verification Results 44 5.2.1 Methodology 44 5.2.2 Verification Results 47 Chapter 6 Conclusions and Future Work 50 Reference 51 | |
| dc.language.iso | en | |
| dc.subject | 資料路徑驗證 | zh_TW |
| dc.subject | 眾數反向圖 | zh_TW |
| dc.subject | 邏輯合成 | zh_TW |
| dc.subject | Logic Synthesis | en |
| dc.subject | Majority-Inverter Graph | en |
| dc.subject | Datapath Verification | en |
| dc.title | 眾數反向圖改寫技術在邏輯合成與驗證之應用 | zh_TW |
| dc.title | Application of DAG-Aware MIG Rewriting Technique in Logic Synthesis and Verification | en |
| dc.type | Thesis | |
| dc.date.schoolyear | 104-2 | |
| dc.description.degree | 碩士 | |
| dc.contributor.oralexamcommittee | 江介宏(Jie-Hong Roland Jiang),王柏堯(Bow-Yaw Wang),許智仁(Chih-Jen Hsu) | |
| dc.subject.keyword | 眾數反向圖,邏輯合成,資料路徑驗證, | zh_TW |
| dc.subject.keyword | Majority-Inverter Graph,Logic Synthesis,Datapath Verification, | en |
| dc.relation.page | 53 | |
| dc.identifier.doi | 10.6342/NTU201601708 | |
| dc.rights.note | 同意授權(全球公開) | |
| dc.date.accepted | 2016-08-02 | |
| dc.contributor.author-college | 電機資訊學院 | zh_TW |
| dc.contributor.author-dept | 電子工程學研究所 | zh_TW |
| 顯示於系所單位： | 電子工程學研究所 | |
文件中的檔案：
| 檔案 | 大小 | 格式 | |
|---|---|---|---|
| ntu-105-1.pdf | 1.54 MB | Adobe PDF | 檢視/開啟 |
系統中的文件，除了特別指名其著作權條款之外，均受到著作權保護，並且保留所有的權利。