Skip navigation

DSpace

機構典藏 DSpace 系統致力於保存各式數位資料(如:文字、圖片、PDF)並使其易於取用。

點此認識 DSpace
DSpace logo
English
中文
  • 瀏覽論文
    • 校院系所
    • 出版年
    • 作者
    • 標題
    • 關鍵字
  • 搜尋 TDR
  • 授權 Q&A
    • 我的頁面
    • 接受 E-mail 通知
    • 編輯個人資料
  1. NTU Theses and Dissertations Repository
  2. 電機資訊學院
  3. 電子工程學研究所
請用此 Handle URI 來引用此文件: http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/94463
完整後設資料紀錄
DC 欄位值語言
dc.contributor.advisor黃鐘揚zh_TW
dc.contributor.advisorChung-Yang Huangen
dc.contributor.author童子瑜zh_TW
dc.contributor.authorTzu-Yu Tungen
dc.date.accessioned2024-08-16T16:12:04Z-
dc.date.available2024-12-27-
dc.date.copyright2024-08-16-
dc.date.issued2024-
dc.date.submitted2024-08-07-
dc.identifier.citation[1] Kai-Fu Tang, Chi-An Wu, Po-Kai Huang, and Chung-Yang Huang. Interpolation-based incremental eco synthesis for multi-error logic rectification. In Proceedings of the 48th Design Automation Conference, pages 146–151, 2011.
[2] Andrew C Ling, Stephen D Brown, Jianwen Zhu, and Sean Safarpour. Towards automated ecos in fpgas. In Proceedings of the ACM/SIGDA international symposium on Field programmable gate arrays, pages 3–12, 2009. 

[3] Kai-FuTang,Po-KaiHuang,Chun-NanChou,andChung-YangHuang.Multi-patch generation for multi-error logic rectification by interpolation with cofactor reduction. In 2012 Design, Automation & Test in Europe Conference & Exhibition (DATE), pages 1567–1572. IEEE, 2012. 

[4] Shao-Lun Huang, Wei-Hsun Lin, Po-Kai Huang, and Chung-Yang Huang. Match and Replace: A Functional ECO Engine for Multierror Circuit Rectification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 32(3):467–478, 2013. 

[5] Smita Krishnaswamy, Haoxing Ren, Nilesh Modi, and Ruchir Puri. Deltasyn: An efficient logic difference optimizer for eco synthesis. In Proceedings of the 2009 International Conference on Computer-Aided Design, pages 789–796, 2009.
[6] Yu-Ling Hsu. Eco patch optimization by rectification point qualification with sat proofs, 2024. Available at http://tdr.lib.ntu.edu.tw/jspui/handle/ 123456789/92142. 

[7] Ai Quoc Dao, Nian-Ze Lee, Li-Cheng Chen, Mark Po-Hung Lin, Jie-Hong R Jiang, Alan Mishchenko, and Robert Brayton. Efficient computation of eco patch functions. In Proceedings of the 55th Annual Design Automation Conference, pages 1–6, 2018. 

[8] Niklas Sorensson and Niklas Een. Minisat v1. 13-a sat solver with conflict-clause minimization. SAT, 2005(53):1–2, 2005. 

[9] An-Che Cheng, Iris Hui-Ru Jiang, and Jing-Yang Jou. Resource-aware functional eco patch generation. In 2016 Design, Automation Test in Europe Conference Exhibition (DATE), pages 1036–1041, 2016. 

[10] AndreasKuehlmann,DavidICheng,ArvindSrinivasan,andDavidPLaPotin.Error diagnosis for transistor-level verification. In Proceedings of the 31st annual Design Automation Conference, pages 218–224, 1994. 

[11] Jie-Hong R Jiang, Victor N Kravets, and Nian-Ze Lee. Engineering change order for combinational and sequential design rectification. In 2020 Design, Automation & Test in Europe Conference & Exhibition (DATE), pages 726–731. IEEE, 2020. 

[12] Victor N Kravets, Nian-Ze Lee, and Jie-Hong R Jiang. Comprehensive search for eco rectification using symbolic sampling. In Proceedings of the 56th Annual Design Automation Conference 2019, pages 1–6, 2019. 

[13] Alexander Stempkovskiy, Dmitry Telpukhov, and Roman Soloviev. Fast and accurate resource-aware functional eco patch generation tool. In 2018 Moscow Workshop on Electronic and Networking Technologies (MWENT), pages 1–6. IEEE, 2018. 

[14] Yu-Neng Wang, Yun-Rong Luo, Po-Chun Chien, Ping-Lun Wang, Hao-Ren Wang, Wan-Hsuan Lin, Jie-Hong Roland Jiang, and Chung-Yang Ric Huang. Compatible equivalence checking of x-valued circuits. In 2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD), pages 1–9. IEEE, 2021. 

[15] Alan Mishchenko, Satrajit Chatterjee, Roland Jiang, and Robert K Brayton. FRAIGs: A Unifying Representation for Logic Synthesis and Verification. Technical report, ERL Technical Report, 2005. 

[16] Armin Biere, Marijn Heule, and Hans van Maaren. Handbook of satisfiability, volume 185. IOS press, 2009. 

[17] ICCAD CAD Contest 2017 Problem A. Resource-aware Patch Generation. https: //iccad-contest.org/2017/CAD-contest-at-ICCAD2017/index.html. Accessed: 2024-01-27. 

[18] Cadence Design Systems, Inc. Logical Equivalence Checking(LEC). License: Conformal_ECO_GXL 21.2. 

[19] Alan Mishchenko. ABC: System for Sequential Logic Synthesis and Formal Verification. https://github.com/berkeley-abc/abc. Accessed: 2024-02-01.
-
dc.identifier.urihttp://tdr.lib.ntu.edu.tw/jspui/handle/123456789/94463-
dc.description.abstract本論文主要探討現代超大規模積體電路(VLSI)設計中工程改變命令(ECO)的問題。由於功能問題和規格變更在設計過程中難以避免,尤其是在接近量產階段時,高效的 ECO 技術對於及時、準確地進行設計修正至關重要,同時避免重複進行邏輯綜合和時序驗證等複雜流程。本研究著重於 ECO 過程的自動化和優化,特別是在選擇和驗證修正區域方面。我們採用改進後基於全稱量詞消除的方法來優化的 ECO 公式。此方法能有效利用 SAT 求解器進行驗證,並探索多樣化的解決方案。我們的主要貢獻在於提出了一種系統性方法來評估和選擇修正區域,從而能夠生成高質量的修補程式。該算法旨在識別多樣化的潛在解法,並確定最佳的修補組合,展示了這種優化方法如何顯著提高 VLSI 設計中 ECO 過程的效率和有效性。通過解決修正區域選擇和驗證的長期挑戰,我們的工作為晶片設計優化的廣泛領域做出了改進。zh_TW
dc.description.abstractThis thesis addresses the critical challenge of Functional Engineering Change Order (ECO) in modern VLSI design. As functional problems and specification changes are inevitable, especially near the tape-out stage, efficient ECO technology is crucial for timely and accurate design corrections without repeating complex processes like logic synthesis and timing verification. The research focuses on automating and optimizing the ECO process, particularly in selecting and verifying rectification regions. We present an innovative algorithm that employs an improved quantifier-elimination based approach for ECO formula manipulation. This method efficiently utilizes SAT solvers for verification and explores a wide variety of solutions. Our key contribution is a systematic approach to evaluating and selecting rectification regions, which enables the generation of high-quality patches. The algorithm is designed to identify diverse potential solutions and determine the optimal combination for patch generation. This approach not only minimizes the risk of overlooking errors but also ensures the maintenance of tight production schedules, which is critical in preventing market entry delays. The thesis demonstrates how this advanced methodology can enhance the efficiency and effectiveness of the ECO process in VLSI design. By addressing the long-standing challenges in rectification region selection and verification, our work contributes to the broader field of chip design optimization.en
dc.description.provenanceSubmitted by admin ntu (admin@lib.ntu.edu.tw) on 2024-08-16T16:12:04Z
No. of bitstreams: 0
en
dc.description.provenanceMade available in DSpace on 2024-08-16T16:12:04Z (GMT). No. of bitstreams: 0en
dc.description.tableofcontentsAcknowledgements i
中文摘要 iii
Abstract iv
Contents vi
List of Figures ix
List of Tables x
Denotation xi
Chapter 1 Introduction 1
1.1 Contributions of the Thesis 2
Chapter 2 Preliminaries 3
2.1 Previous Works on the ECO Problem 3
2.2 Boolean Satisfiability 4
2.3 AIG & FRAIG 4
2.4 Equivalence Checking 5
2.5 Quantified Boolean Formula 6
2.6 De Morgan’s Laws and Quantifier Elimination 7
2.7 Unate Function 8
Chapter 3 Main Algorithm and Overall Architecture 9
3.1 Motivation 9
3.2 Formulation of Rectification Point Selection Problem 11
3.3 Quantifier Elimination Process 12
3.3.1 Universal Quantifier Elimination 12
3.3.2 Quantifier Elimination on Unate Gate 13
3.3.3 Multiple Fanout Situation 15
3.3.4 Quantifier Elimination on the Miter 16
3.3.5 Auxiliary Decision Variables 17
3.3.6 Multiple POs Situation 19
3.4 The Architecture of Our Framework 20
Chapter 4 Implementation 23
4.1 Preparation 23
4.1.1 Miter 23
4.1.2 CNF Construction 24
4.2 Rectification Point Candidates Evaluation 25
4.2.1 Counter Example Generation 25
4.2.2 Suspicious Score Computation 26
4.2.3 Functional and Structural Similarity 30
4.2.4 CandidateSelection 31
4.3 Rectification Point Sets Verification 31
4.3.1 X-value Simulation 31
4.3.2 Unateness Identification 33
4.3.3 CNF Construction with Quantifier Elimination 35
4.3.4 UNSAT Core Extraction 36
4.3.4.1 Selecting Stage 36
4.3.4.2 Verifying Equivalence Stage 37
4.3.5 Overall Strategy 38
4.4 Patch Generation 39
4.4.1 Sorting Criteria 39
4.4.1.1 Rectification Points Similarity 39
4.4.1.2 Level Summation 40
4.4.2 Simulated Annealing 41
Chapter 5 Experimental Results 43
5.1 Important Metrics Explanation 44
5.2 Testcases with Handicraft Bugs 44
5.3 2017 CAD Contest Testcases 47
5.4 Solution Sets Sorting Comparison 47
5.5 Patch Costs under Different Conditions 50
5.6 Comparison and Analysis 51
Chapter 6 Conclusion and Future Directions 53
References 55
-
dc.language.isoen-
dc.title工程改變命令補丁生成的最佳矯正點選擇zh_TW
dc.titleOptimal Rectification Point Selection for Functional ECO Patch Generationen
dc.typeThesis-
dc.date.schoolyear112-2-
dc.description.degree碩士-
dc.contributor.oralexamcommittee江介宏;黃紹倫;林彥德zh_TW
dc.contributor.oralexamcommitteeJie-Hong Jiang;Shao-Lun Huang;Yen-Te Linen
dc.subject.keyword工程改變命令,校正點,可滿足性問題,邏輯電路,量化布林公式,zh_TW
dc.subject.keywordECO,Rectification Point,SAT,Logic Circuit,QBF,en
dc.relation.page57-
dc.identifier.doi10.6342/NTU202403757-
dc.rights.note未授權-
dc.date.accepted2024-08-10-
dc.contributor.author-college電機資訊學院-
dc.contributor.author-dept電子工程學研究所-
顯示於系所單位:電子工程學研究所

文件中的檔案:
檔案 大小格式 
ntu-112-2.pdf
  目前未授權公開取用
7.71 MBAdobe PDF
顯示文件簡單紀錄


系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。

社群連結
聯絡資訊
10617臺北市大安區羅斯福路四段1號
No.1 Sec.4, Roosevelt Rd., Taipei, Taiwan, R.O.C. 106
Tel: (02)33662353
Email: ntuetds@ntu.edu.tw
意見箱
相關連結
館藏目錄
國內圖書館整合查詢 MetaCat
臺大學術典藏 NTU Scholars
臺大圖書館數位典藏館
本站聲明
© NTU Library All Rights Reserved