針對時序重置與重新合成之循序電路等效驗證問題所提出之改良式性質導向可達度技術

Improving Property Directed Reachability Techniques for Sequential Equivalence Checking under Retiming and Resynthesis

徐筱芸(Sheau-Yun Hsu)

指導教授 ： 黃鐘揚

國立臺灣大學/電機資訊學院/電子工程學研究所/碩士(2014年)

https://doi.org/10.6342/NTU.2014.02042

摘要

循序電路等效驗證是一個在應用上重要且實際的問題。過去，等效驗證通常被當成一般的性質驗證問題處理，或者是藉由找到一組可用歸納法證明的等效訊號來解決，然而，無論採用哪一種方式，在解決循序電路等效驗證問題上都會遇到很多困難之處。在這篇論文裡，我們研究了一些相關的技術並且提出一個混和性的驗證方法，這個方法在使用一般的性質驗證技術的同時，考量了電路中等效的訊號，是結合兩種不同的做法改良式版本。

關鍵字

循序電路等效驗證 ； 性質導向可達度 ； 時序重置 ； 布林可滿足性問題

並列摘要

Sequential equivalence checking is an important practical problem. Previously, sequential equivalence checking problems are either treated as general property checking problems or solved by finding an inductive set of internal equivalent signals. However, difficulties are encountered by either approach. In this thesis, we study several related techniques and derive a hybrid method that allows a property checking engine to utilize functionally equivalent signals to prove the equivalence of both circuits. Our method shows a bridge between very different approaches.

並列關鍵字

SEC ； PDR ； Retime ； SAT

參考文獻

[9] C.-Y. Wu and C.-Y. R. Huang. V3: An Extensible Framework for Hardware Verification. http://dvlab.ee.ntu.edu.tw/~publication/V3/

[1] C. A. J. van Eijk. Sequential equivalence checking based on structural similarities. IEEE Trans. Computer-Aided Design, pp 814-819, July 2000.

[2] J.-H. R. Jiang and W.-L. Hung. Inductive Equivalence Checking under Retiming and Resynthesis. IEEE Trans. Computer-Aided Design, pp 326-333, November 2007.

[4] N. Liveris, H. Zhou and P. Banerjee. Complete-k-Distinguishability for Retiming and Resynthesis Equivalence Checking without Restricting Synthesis. Asia and South Pacific Design Automation Conference (ASP-DAC), pp 636-641, 2009.

[6] R. Brayton, N. Een and A. Mishchenko. Using Speculation for Sequential Equivalence Checking. Proc. International Workshop on Logic and Synthesis (IWLS), 2012.