(3.235.108.188) 您好!臺灣時間:2021/03/07 21:26
字體大小: 字級放大   字級縮小   預設字形  
回查詢結果

詳目顯示:::

我願授權國圖
: 
twitterline
研究生:徐筱芸
研究生(外文):Sheau-Yun Hsu
論文名稱:針對時序重置與重新合成之循序電路等效驗證問題所提出之改良式性質導向可達度技術
論文名稱(外文):Improving Property Directed Reachability Techniques for Sequential Equivalence Checking under Retiming and Resynthesis
指導教授:黃鐘揚
口試委員:李建模江介宏王柏堯
口試日期:2014-07-28
學位類別:碩士
校院名稱:國立臺灣大學
系所名稱:電子工程學研究所
學門:工程學門
學類:電資工程學類
論文種類:學術論文
論文出版年:2014
畢業學年度:102
語文別:英文
論文頁數:55
中文關鍵詞:循序電路等效驗證性質導向可達度時序重置布林可滿足性問題
外文關鍵詞:SECPDRRetimeSAT
相關次數:
  • 被引用被引用:0
  • 點閱點閱:78
  • 評分評分:系統版面圖檔系統版面圖檔系統版面圖檔系統版面圖檔系統版面圖檔
  • 下載下載:0
  • 收藏至我的研究室書目清單書目收藏:0
循序電路等效驗證是一個在應用上重要且實際的問題。過去,等效驗證通常被當成一般的性質驗證問題處理,或者是藉由找到一組可用歸納法證明的等效訊號來解決,然而,無論採用哪一種方式,在解決循序電路等效驗證問題上都會遇到很多困難之處。在這篇論文裡,我們研究了一些相關的技術並且提出一個混和性的驗證方法,這個方法在使用一般的性質驗證技術的同時,考量了電路中等效的訊號,是結合兩種不同的做法改良式版本。

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/


QRCODE
 
 
 
 
 
                                                                                                                                                                                                                                                                                                                                                                                                               
第一頁 上一頁 下一頁 最後一頁 top
系統版面圖檔 系統版面圖檔