應用模塊分析提升性質導向可達度技術

Abstract

隨著數位電路規模快速成長，對於模式驗證效率的要求也越來越高，近年來各種針對模式驗證的演算法如雨後春筍般出現，其中最具代表性的就是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.