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

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.

口試委員會審定書 #
致謝 i
中文摘要 ii
ABSTRACT iii
CONTENTS iv
LIST OF FIGURES vi
LIST OF TABLES vii
Chapter 1 Introduction 1
Chapter 2 Priliminaries 3
2.1 Circuits 3
2.1.1 Miter circuits and exquivalence checking 3
2.1.2 Timeframe expansion. 4
2.2 Invariants 4
2.3 Property Checking 6
2.3.1 Satisfiability problem 6
2.3.2 K-induction. 6
2.3.2 Property directed reachability. 7
2.3.2 Sequential equivalence checking. 9
Chapter 3 Problem Analysis 10
3.1 Retiming Invariant 10
3.2 Computation of Invariants in PDR 12
3.3 Constraining Power of Invariants in PDR 15
3.4 Motivation of Modified PDR 17
Chapter 4 Related Works 19
4.1 Inductive Equivalence Checking 19
4.1.1 Inductive signal correspondence 19
4.1.2 Constuction of equivalence candidates 22
4.1.3 Limitation 25
4.2 Equivalence Checking Using Speculation 25
4.2.1 Speculatively reduced model 25
4.2.2 Equivalence checking 26
4.3 Comparison 26
Chapter 5 Modified PDR 28
5.1 Overall Flow 28
5.2 Candidate Construction 29
5.2.1 Random simulation and rarity simulation 30
5.2.2 Candidate filtering 31
5.3 Invariant Propagation 32
5.3.1 Extended inductive model 33
5.3.2 Forward propagation using UNSAT proof 35
5.3.3 Candidate prioritizing 36
5.3.4 Other methods 37
Chapter 6 Experimental Result 40
6.1 Comparison to Original PDR 40
6.2 Comparison to Inductive Approach 44
6.3 Invariant Prioritizing and Removal 46
Chapter 7 Conclusion 54
REFERENCE 55

[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.
[3]N. Een, A. Mishchenko and R. Brayton. Efficient Implementation of Property Directed Reachability. In Formal Methods in Computer-Aided Design (FMCAD), pp 125-134, 2011.
[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.
[5]M. Mneimneh and K. Sakallah. REVERSE: Efficient Sequential Verification for Retiming. Proc. International Workshop on Logic and Synthesis (IWLS), pp 133-139, 2003.
[6]R. Brayton, N. Een and A. Mishchenko. Using Speculation for Sequential Equivalence Checking. Proc. International Workshop on Logic and Synthesis (IWLS), 2012.
[7]W. Hu, H. Nguyen and M. S. Hsiao. Sufficiency-based Filtering of Invariants for Sequential Equivalence Checking. High Level Design Validation and Test Workshop (HLDVT), pp 1-8, November 2011.
[8]Berkeley Logic Synthesis and Verification Group. ABC: A System for Sequential Synthesis and Verification. http://www.eecs.berkeley.edu/~alanmi/abc/
[9]C.-Y. Wu and C.-Y. R. Huang. V3: An Extensible Framework for Hardware Verification. http://dvlab.ee.ntu.edu.tw/~publication/V3/