請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/65240
完整後設資料紀錄
DC 欄位 | 值 | 語言 |
---|---|---|
dc.contributor.advisor | 黃鐘揚(Chung-Yang Huang) | |
dc.contributor.author | Wei-Hsun Lin | en |
dc.contributor.author | 林暐勛 | zh_TW |
dc.date.accessioned | 2021-06-16T23:32:04Z | - |
dc.date.available | 2015-08-03 | |
dc.date.copyright | 2012-08-03 | |
dc.date.issued | 2012 | |
dc.date.submitted | 2012-07-29 | |
dc.identifier.citation | [1] Andreas G. Veneris and Ibrahim N. Hajj. Design error diagnosis and correction via test vector simulation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 18(12): 1803-1816, 2006.
[2] Kai-Hui Chang, Igor L. Markov, and Valeria Bertacco. Fixing design errors with counterexamples and resynthesis. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 27(1): 184-188, 2008. [3] Bo-Han Wu, Chun-Ju Yang, Chung-Yang Huang, and Jie-Hong Roland Jiang. A robust functional ECO engine by SAT proof minimization and interpolation techniques. In Proceedings of International Conference on Computer-Aided Design, pages 729–734, 2010. [4] Kai-Fu Tang, Chi-An Wu, Po-Kai Huang, and Chung-Yang (Ric) Huang. Interpolation-based incremental ECO synthesis for multi-error logic rectification. In Proceedings of Design Automation Conference, pages 146–151, 2011. [5] Kai-Fu Tang, Po-Kai Huang, Chun-Nan Chou, and Chung-Yang Huang. Multi-patch generation for multi-error logic rectification by interpolation with cofactor reduction. In Proceedings of Design, Automation & Test in Europe, pages 1567–1572, 2012. [6] Shao-Lun Huang, Wei-Hsun Lin, and Chung-Yang (Ric) Huang. Match and replace - a functional ECO engine for multi-error circuit rectification. In Proceedings of International Conference on Computer-Aided Design, pages 383–388, 2011. [7] Edmund M. Clarke, Orna Grumberg, and Doron Peled. Model checking. MIT Press, 2001. [8] Armin Biere, Cyrille Artho, and Viktor Schuppan. Liveness checking as safety checking. Electronic Notes in Theoretical Computer Science, 66(2):160–177, 2002. [9] Bowen Alpern and Fred B. Schneider. Defining liveness. Information Processing Letters, 21(4):181–185, 1985. [10] Fred B. Schneider. Decomposing properties into safety and liveness using predicate logic. Technical report, pages 87–874, Cornell University, 1987. [11] Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. Symbolic model checking without BDDs. In Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 193–207, 1999. [12] Stephen A. Cook. The complexity of theorem-proving procedures. In Symposium on the Theory of Computing, pages 151–158, 1971. [13] Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of Design Automation Conference, pages 530–535, 2001. [14] Niklas Een and Niklas Sorensson. An extensible SAT-solver. In Proceedings of International Conferences on Theory and Applications of Satisfiability Testing, pages 502–518, 2003. [15] Jie-Hong Roland Jiang and Wei-Lun Hung. Inductive equivalence checking under retiming and resynthesis. In Proceedings of International Conference on Computer-Aided Design, pages 326–333, 2007. [16] Jie-Hong Roland Jiang and Robert K. Brayton. Retiming and resynthesis: A complexity perspective. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 25(12):2674–2686, 2006. [17] C. A. J. van Eijk. Sequential equivalence checking without state space traversal. In Proceedings of Design, Automation & Test in Europe, pages 618–623, 1998. [18] Alan Mishchenko, Michael L. Case, Robert K. Brayton, and Stephen Jang. Scalable and scalably-verifiable sequential synthesis. In Proceedings of International Conference on Computer-Aided Design, pages 234–241, 2008. [19] Aaron R. Bradley. SAT-based model checking without unrolling. In Proceedings of International Conference on Verification, Model Checking, and Abstract Interpretation, pages 70–87, 2011. [20] Niklas Een, Alan Mishchenko, and Robert K. Brayton. Efficient implementation of property directed reachability. In Proceedings of Formal Methods in Computer-Aided Design, 2011. [21] Kenneth L. McMillan. Interpolation and SAT-based model checking. In Proceedings of International Conference on Computer Aided Verification, pages 1–13, 2003. [22] Gorschwin Fey, Sean Safarpour, Andreas G. Veneris, and Rolf Drechsler. On the relation between simulation-based and SAT-based diagnosis. In Proceedings of Design, Automation & Test in Europe, pages 1139–1144, 2006. [23] Berkeley Logic Synthesis and Verification Group. ABC: A system for sequential synthesis and verification. http://www.eecs.berkeley.edu/~alanmi/abc/ | |
dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/65240 | - |
dc.description.abstract | 在超大型積體電路設計階段中,功能修正已變成一個不可或缺的過程。傳統上,功能修正藉由許多組合電路的技術而達成,然而其並沒有考慮暫存器對於功能改變的彈性,因此,這些組合電路的技術並沒有辦法直接使用在有不匹配暫存器的循序電路上。在這篇論文中,我們提出了一個修正循序電路的方法,其使用了必然性模型檢測技術來檢驗舊設計電路與新規格電路的可修正性。此外,我們利用了內插邏輯技術來產生修正函數,並藉由找尋較好的基底變數,加速了整體修正過程。實驗結果顯示我們所提出的方法可以有效率地決定一個給定的信號是否可以將電路修正,並且能有效地產生夠小的修正函數。最後,我們的方法提供了組合性修正另一條路,而且可於大部分的實驗中產生較小的修正函數。 | zh_TW |
dc.description.abstract | Functional rectification has been an indispensable process in late VLSI design stages. Traditionally, functional rectification is achieved by various techniques on combinational circuits. It does not explore the flexibility of functional changes across the register boundary. As a result, these combinational rectification techniques cannot be applied directly to sequential circuits with unmatched registers. In this thesis, we propose a sequential rectification approach, which utilizes the liveness model checking techniques to facilitate checking of the sequential rectifiability between old implementation and golden specification. In addition, we apply the interpolation technique to construct the rectification function (i.e. the patch). By identifying better supports for the patch generation, we demonstrate that the whole procedure can be accelerated. Experimental results show that our method can efficiently determine whether a given signal is a rectification signal and find the patch circuits effectively. In the end, our method can provide an alternative way to the combinational rectification and it generates smaller in most of cases. | en |
dc.description.provenance | Made available in DSpace on 2021-06-16T23:32:04Z (GMT). No. of bitstreams: 1 ntu-101-R99943090-1.pdf: 565701 bytes, checksum: b49945b8b6df8338fa27701809056aa8 (MD5) Previous issue date: 2012 | en |
dc.description.tableofcontents | 誌謝 i
中文摘要 ii ABSTRACT iii CONTENTS iv LIST OF FIGURES vi LIST OF TABLES viii Chapter 1 Introduction 1 Chapter 2 Preliminary 4 2.1 Model Checking 4 2.1.1 Temporal Logic 4 2.1.2 Safety Property 5 2.1.3 Liveness Property 5 2.1.4 Liveness Checking as Safety Checking 6 2.2 Bounded Model Checking 7 2.2.1 Boolean Satisfiability Problem 7 2.2.2 Bounded Model Checking on Safety Properties 7 2.3 Equivalence Checking 9 2.3.1 Combinational Equivalence Checking 9 2.3.2 Sequential Equivalence Checking 10 2.4 Craig Interpolation 12 2.4.1 Resolution Graph of Unsatisfiability Proof 13 2.4.2 McMillan’s Algorithm 13 2.5 Combinational Engineering Change Order 15 2.5.1 Sweeping-based ECO 16 2.5.2 Diagnosis-based ECO 16 2.6 Problem Formulation 18 Chapter 3 Single Rectification on Sequential Circuits without Inputs 20 3.1 Algorithm Overview 20 3.2 Constrained Liveness Property for Rectification 22 3.3 Rectifiability Checking by Liveness Model Checking 26 3.4 Patch Generation via Interpolation 29 3.5 Identification of Better Supports to Patch Functions 30 3.6 Summary and Discussion 34 Chapter 4 Single Rectification on General Circuits 36 4.1 Algorithm Overview 36 4.2 Constrained Liveness Property under Single Error Trace 38 4.3 Constrained Liveness Property under Multiple Error Traces 41 4.4 Incremental Rectification 43 4.5 Summary 46 Chapter 5 Experimental Results 47 Chapter 6 Conclusions and Future Work 54 REFERENCE 55 | |
dc.language.iso | en | |
dc.title | 利用必然性模型檢測技術所進行之循序電路功能修正 | zh_TW |
dc.title | Functional Rectification on Sequential Circuits by Liveness Model Checking Techniques | en |
dc.type | Thesis | |
dc.date.schoolyear | 100-2 | |
dc.description.degree | 碩士 | |
dc.contributor.oralexamcommittee | 江介宏(Jie-Hong Jiang),江蕙如(Hui-Ru Jiang),顏嘉志(Chia-Chih Yen) | |
dc.subject.keyword | 功能修正,必然性性質,模型檢測, | zh_TW |
dc.subject.keyword | Functional Rectification,Liveness Property,Model Checking, | en |
dc.relation.page | 57 | |
dc.rights.note | 有償授權 | |
dc.date.accepted | 2012-07-30 | |
dc.contributor.author-college | 電機資訊學院 | zh_TW |
dc.contributor.author-dept | 電子工程學研究所 | zh_TW |
顯示於系所單位: | 電子工程學研究所 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
ntu-101-1.pdf 目前未授權公開取用 | 552.44 kB | Adobe PDF |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。