請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/52350
標題: | 應用模塊分析提升性質導向可達度技術 Enhancing Property Directed Reachability Technique through Cube Analysis |
作者: | Hong-Syun Jiang 江弘勛 |
指導教授: | 黃鐘揚(Chung-Yang (Ric) |
關鍵字: | 模式驗證,性質導向可達度,模塊分析,循序電路驗證, Model Checking,Safety Property Checking,Property Directed Reachability,Sequential Verification, |
出版年 : | 2015 |
學位: | 碩士 |
摘要: | 隨著數位電路規模快速成長,對於模式驗證效率的要求也越來越高,近年來各種針對模式驗證的演算法如雨後春筍般出現,其中最具代表性的就是2011年由Aaron Bradley與Niclas Een發表的性質導向可達度技術,直到現在該技術依然是解決大多數模式驗證問題最有效的方法,然而隨著電路越趨複雜規模越來越龐大,許多電路驗證問題仍然無法在可接受的時間內解決,因此本篇論文針對性質導向可達度技術進行分析,並提出三個不同的變形,再藉由對於解題時產生的模塊進行分析決定該使用何種變形,企圖提升性質導向可達度技術之效率,解決更多模式驗證問題. Sequential verification is an important practical problem in these years. But it is hard to solved, both model checking and equivalence checking. There are many different techniques solving this problem such as BMC, ITP, and PDR. In all these different techniques, the recently developed PDR works best. Nevertheless, restricted by its NP complexity, many sequential verification problems remain unsolved. In this thesis we focus on how PDR work on these problems, and construct a cube analysis method try to figure out the bottleneck of PDR. Through the analysis we generate three different algorithms to help PDR get better performance. At the end we integrate all three methods and the original PDR in order to seek complete improvement on hardware model checking problem. |
URI: | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/52350 |
全文授權: | 有償授權 |
顯示於系所單位: | 電子工程學研究所 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
ntu-104-1.pdf 目前未授權公開取用 | 2.2 MB | Adobe PDF |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。