請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/91705
完整後設資料紀錄
DC 欄位 | 值 | 語言 |
---|---|---|
dc.contributor.advisor | 黃鐘揚 | zh_TW |
dc.contributor.advisor | Chung-Yang Huang | en |
dc.contributor.author | 林嘉豪 | zh_TW |
dc.contributor.author | Jia-Hao Lin | en |
dc.date.accessioned | 2024-02-22T16:19:47Z | - |
dc.date.available | 2024-02-23 | - |
dc.date.copyright | 2024-02-22 | - |
dc.date.issued | 2023 | - |
dc.date.submitted | 2024-01-28 | - |
dc.identifier.citation | 1. V. Guarnieri, G. Di Guglielmo, N. Bombieri et al., “On the reuse of TLMmutation analysis at RTL,” Journal of Electronic Testing, vol. 28, no. 4, pp. 435–448, 2012.
2. N. Bombieri,G.Di Guglielmo,M. Ferrari et al., “HIFSuite: tools For HDL code conversion andmanipulation,” Eurasip Journal on Embedded Systems, vol. 2010, Article ID 436328, 2010. 3. S. Shyam and V. Bertacco, "Distance-guided hybrid verification with GUIDO", Proc. Design Autom. Test Eur. Conf. Exhibit. (DATE), pp.1-6, Mar. 2006. 4. Yanhong Zhou, Tiancheng Wang, Huawei Li, Tao Lv and Xiaowei Li, "Functional test generation for hard-to-reach states using path constraint solving", IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 35, no. 6, pp. 999-1011, 2015. 5. Yuan Lu; Weimin Li, "A semi-formal verification methodology," ASIC, 2001. Proceedings. 4th International Conference on, 2001. 6. S. Gorai, S. Biswas, L. Bhatia, P. Tiwari and R. S. Mitra, "Directedsimulation assisted formal verification of serial protocol and bridge", 2006 43rd ACM/IEEE Design Automation Conference, pp. 731-736, 2006. 7. Richard Ho, et al., “Post-Silicon Debug Using Formal Verification Waypoints,” DVCon 2009 8. Blaine Hsieh, et al., “Every Cloud - Post-Silicon Bug Spurs Formal Verification Adoption,” DVCon 2015 9. Eslinger and Yeung. “Formal Bug Hunting with River Fishing Techniques”, DVCON 2019. 10. V. Guarnieri, G. Di Guglielmo, N. Bombieri et al., “On the reuse of TLMmutation analysis at RTL,” Journal of Electronic Testing, vol. 28, no. 4, pp. 435–448, 2012. 11. N. Bombieri,G.Di Guglielmo,M. Ferrari et al., “HIFSuite: tools For HDL code conversion andmanipulation,” Eurasip Journal on Embedded Systems, vol. 2010, Article ID 436328, 2010. 12. McMillan, Kenneth L., and Kenneth L. McMillan. Symbolic model checking. Springer US, 1993. 13. Kang, Hyeong-Ju, and In-Cheol Park. "SAT-based unbounded symbolic model checking." Proceedings of the 40th annual Design Automation Conference. 2003. 14. McMillan, Kenneth L. "Interpolation and SAT-based model checking." Computer Aided Verification: 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003. Proceedings 15. Springer Berlin Heidelberg, 2003. 15. I. C. S. D. A. S. Committee, IEEE standard for SystemVerilog--unified hardware design, specification, and verification language, 2nd ed. New York: Institute of Electrical and Electronics Engineers, 2010. 16. Yunfeng Tao, "An introduction to assertion-based verification," ASIC, 2009. ASICON ''09. IEEE 8th International Conference on, Oct. 2009 17. Y. Shi, C. W. Ting, B.-H. Gwee, and Y. Ren, "A highly efficient method for extracting FSMs from flattened gate-level netlist," in 2010 IEEE56International Symposium on Circuits and Systems - ISCAS 2010, Paris,France, May 30–Jun. 2, 2010. 18. “Synopsys VC Formal” https://www.synopsys.com/verification/staticand-formal-verification/vc-formal.html 19. “vcdvcd” https://github.com/cirosantilli/vcdvcd 20. N. Een, A. Mishchenko and N. Amla, "A single-instance incremental sat formulation of proof-and counterexample-based abstraction" in Formal Methods in Computer-Aided Design (FMCAD) 2010, IEEE, pp. 181-188, 2010. 21. N. Eén, A. Mishchenko, and R. Brayton, "Efficient implementation of property directed reachability," in Formal Methods in Computer-Aided Design (FMCAD) pp. 125-134, October, 2011. 22. “PicoSoc” https://github.com/YosysHQ/picorv32 23. “Google RISCV-DV” https://github.com/chipsalliance/riscv-dv 24. “Yosys Open SYnthesis Suite.” https://yosyshq.net/yosys | - |
dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/91705 | - |
dc.description.abstract | 隨着系統晶片的複雜性呈指數級增長,且製作先進製程晶片的成本逐步提高,考量到上市時間和ECO所需的資金壓力,驗證程序已成為晶片設計流程中不可或缺的要素。在眾多主流的驗證方法中,基於模擬的約束隨機驗證方法通過對系統行為進行隨機模擬,以提升驗證的可靠性。這些方法以代碼覆蓋率、分支覆蓋率、狀態機覆蓋率以及功能覆蓋率等指標來衡量設計的可靠性。然而,這些指標僅關注於錯誤發生的特定狀態,而忽略了可能導致系統錯誤的訊號傳播,這最終構成了潛在風險。要識別潛在錯誤,需要對各種情況進行模擬。因此,在本研究中,我們將正規驗證方法和模擬驗證方法相結合,以找出可能導致錯誤的各種狀態。同時,也克服了正規驗證在處理大型設計方面的局限性。最終,我們在一個複雜設計中應用了這一方法,成功地發現了兩個潛在系統錯誤。這些錯誤無法單獨通過模擬驗證或正規驗證方法發現,但通過我們的方法得以揭示。 | zh_TW |
dc.description.abstract | The verification process has become an essential component in the chip design workflow due to the exponential growth in the complexity of system chips and the gradual increase in manufacturing costs for advanced process chips. Simulationbased constrained random verification is a widely used technique in the field of verification. This method improves the dependability of the verification process by subjecting the system behavior to random simulations. These methodologies utilize many metrics, including code coverage, branch coverage, state machine coverage, and functional coverage[1][2], to assess the reliability of a design. Nevertheless, the aforementioned measures primarily concentrate on individual states where faults are observed, disregarding the transmission of signals that could potentially result in system mistakes, thereby presenting possible hazards.
In order to detect hidden flaws, it is necessary for simulations to encompass arange of scenarios. Therefore, this study aims to integrate formal verification approaches with simulation-based verification methods in order to detect various states that have the potential to result in mistakes. In the final analysis, we implement this methodology to an intricate design and effectively discover two potential system flaws. These mistakes are not easily detected using standalone simulation-based or formal verification approaches, but our approach is able to uncover them. | en |
dc.description.provenance | Submitted by admin ntu (admin@lib.ntu.edu.tw) on 2024-02-22T16:19:47Z No. of bitstreams: 0 | en |
dc.description.provenance | Made available in DSpace on 2024-02-22T16:19:47Z (GMT). No. of bitstreams: 0 | en |
dc.description.tableofcontents | 誌謝 ...i
中⽂摘要 ...ii ABSTRACT ...iii CONTENTS ...iv LIST OF FIGURES ...vi LIST OF TABLES ...viii Chapter 1 Introduction ...1 1.1 Motivation ...1 1.2 Related Work ...3 1.3 Contributions ...5 1.4 Thesis Organization ...6 Chapter 2 Background Knowledge ...7 2.1 Functional Verification in Design Flow ...7 2.2 Hierarchy Verificaiton ...9 2.3 Simulation-Based Verification ...11 2.4 Coverage Metrics ...13 2.5 Formal-Based Verification ...14 2.6 SystemVerilog Assertions ...17 Chapter 3 Overview of Counterexample-Guided Hybrid Approach ...18 3.1 The Architecture of Our Framework ...18 3.2 Abstract Engine ...21 3.3 Sampling Phase ...23 3.4 Candidate Generalization ...28 3.5 Sequential Constraint Extraction ...29 3.6 Waypoint Phase ...31 3.7 Proof Phase ...33 Chapter 4 Experimental Results ...34 4.1 A Brief Overview of the Design Under Verification ...34 4.2 Testbench Architecture ...36 4.3 Simulation-Based Results ...42 4.4 Formal-Based Results ...43 4.5 Our Approach Results ...43 Chapter 5 Conclusion ...46 REFERENCES ...47 | - |
dc.language.iso | en | - |
dc.title | 序列特定目標識別和正規證明在系統層級設計中的錯誤路徑生成 | zh_TW |
dc.title | Bug Trace Generation by Sequential Waypoint Identification and Formal Proof for System-Level Designs | en |
dc.type | Thesis | - |
dc.date.schoolyear | 112-1 | - |
dc.description.degree | 碩士 | - |
dc.contributor.oralexamcommittee | 黃紹倫;莊咸和;楊欣嘉 | zh_TW |
dc.contributor.oralexamcommittee | Shao-Lun Huang;Hsien-He Chuang;Hsin-Chia Yang | en |
dc.subject.keyword | 功能性測試,限制隨機驗證,正規驗證,半正規驗證,模擬驗證, | zh_TW |
dc.subject.keyword | Functional Testing,Constrained Random Verification,Formal Verification,Semi-Formal Verification,Simulation-Based Verification, | en |
dc.relation.page | 49 | - |
dc.identifier.doi | 10.6342/NTU202400220 | - |
dc.rights.note | 未授權 | - |
dc.date.accepted | 2024-01-30 | - |
dc.contributor.author-college | 電機資訊學院 | - |
dc.contributor.author-dept | 電子工程學研究所 | - |
顯示於系所單位: | 電子工程學研究所 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
ntu-112-1.pdf 目前未授權公開取用 | 4.97 MB | Adobe PDF |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。