使用機率進行組合電路之等效驗證｜國立清華大學博碩士論文庫

簡易檢索 / 詳目顯示

回結果列表

研究生：	吳世傑 Shih-Chieh Wu
論文名稱：	使用機率進行組合電路之等效驗證 Combinational Equivalence Checking Using Probability
指導教授：	王俊堯 Chun-Yao Wang
口試委員:
學位類別：	碩士 Master
系所名稱：	電機資訊學院 - 資訊工程學系 Computer Science
論文出版年：	2006
畢業學年度：	94
語文別：	中文
論文頁數：	40
中文關鍵詞：	機率方法、等效驗證、組合電路、機率驗證架構
外文關鍵詞：	probabilistic approach, equivalence checking, combinational circuits, PEACH
相關次數：	點閱：1 下載：0
分享至:	分享至facebook 分享至twitter

查詢本校圖書館目錄查詢臺灣博碩士論文知識加值系統勘誤回報

本論文提出以機率為基礎的方法來對組合電路進行等效驗證。論文中首先會介紹一個精確的方法來進行等效驗證—此方法使用特定的機率值給法使得每個電路有唯一的輸出機率值，為了改善機率運算的效率，我們提出了新的編碼方法以及運算子來加快輸出機率的計算，此編碼方法和運算子同時也解決了輸出機率計算過程中的信號相關問題，然而，此精確方法所使用的特定機率值會呈現指數性的成長，這個固有的缺點限制了精確方法解決大電路的能力；因此，論文接下來會介紹一個近似的方法來進行等效驗證，我們提出一種驗證的架構—PEACH，此架構使用一次的機率計算過程便可得到輸出機率值，雖然此輸出機率值並不唯一，但其發生錯誤的機率相當低—接近於零，並且設計者還可以藉由調整架構中的參數來得到較低的錯誤發生機率。

This thesis presents probability based approaches to combinational equivalence checking. First, an exact approach using aliasing-free assignments is introduced. To improve the efficiency of probability calculation, a new encoding scheme and operations are proposed. The encoding scheme and operations also solve the signal correlation issue during the output probability calculation. However, the aliasing-free assignments exponentially grow. This
inherent disadvantage limits the exact approach to solve large circuits. Thus, an approximate approach is proposed. We propose a verification architecture, PEACH, such that a virtually-zero aliasing rate is obtained in a single-pass probability calculation. Furthermore, the aliasing rate can be easily configured in various precision by designers.

Contents
摘要.......................................................................................................................................... i
Abstract.................................................................................................................................... ii
Acknowledgements................................................................................................................iii
Contents.................................................................................................................................. iv
List of Figures........................................................................................................................ vi
List of Tables.........................................................................................................................viii
Chapter 1 Introduction.............................................................................................................1
1.1 Motivation..................................................................................................................1
1.2 Problem Formulation ................................................................................................2
1.3 Existing Approaches to CEC....................................................................................2
1.4 Our Contributions......................................................................................................4
1.5 Overview....................................................................................................................5
Chapter 2 Background.............................................................................................................6
2.1 Probability Expression..............................................................................................6
2.2 Numerical Computation............................................................................................8
2.2.1 Aliasing Problem............................................................................................8
2.2.2 Signal Correlation Problem...........................................................................9
2.3 Aliasing-Free Assignments.......................................................................................9
Chapter 3 Exact Approach.....................................................................................................12
3.1 Encoding Scheme....................................................................................................12
3.2 Alternative Operations ............................................................................................13
3.3 Dealing with Signal Correlation.............................................................................15
3.4 Limitation ................................................................................................................17
Chapter 4 Approximate Approach ........................................................................................18
4.1 PEACH Architecture...............................................................................................18
4.2 Aliasing Rate Analysis............................................................................................21
Chapter 5 Experimental Results and Analysis .....................................................................27
5.1 Experimental Setup.................................................................................................27
5.2 Experimental Results of Exact Approach..............................................................27
5.3 Experimental Results of Approximate Approach..................................................29
5.3.1 Verifying Two Equivalent Netlists..............................................................29
5.3.2 Verifying Two Non-Equivalent Netlists .....................................................32
5.3.3 Analysis ........................................................................................................33
Chapter 6 Conclusions...........................................................................................................37
References.............................................................................................................................38

                                

References
[1] M. S. Abadir, et al., ”Logic Verification via Test Generation,” IEEE Trans. on Computer
Aided-Design, pp. 138-148, Jan. 1988.
[2] J. Hu Alan, ”Formal Hardware Verification with BDDs: An Introduction,” in Proc. of
PACRIM, pp. 677-682, 1997.
[3] V. D. Agrawal, et al., ”Characteristic Polynomial Method for Verification and Test of
Combinational Circuits,” in Proc. of Int. Conf. on VLSI Design, pp. 341-342, 1996.
[4] D. Brand, ”Verification of Large Synthesized Designs,” in Proc. of ICCAD, pp. 534-
539, 1993.
[5] R. E. Bryant, ”Graph-based Algorithms for Boolean Function Manipulation,” IEEE
Trans. on Computers, pp. 677-691, Aug. 1986.
[6] R. E. Bryant, ”Binary Decision Diagrams and Beyond: Enabling Technologies for
Formal Verification,” in Proc. of ICCAD, pp. 236-243, 1995.
[7] E. I. Goldberg, et al., ”Using SAT for Combinational Equivalence Checking,” in
Proc. of DATE, pp. 114-121, 2001.
[8] A. Hett, et al., ”Fast and Ecient Construction of BDDs,” in Proc. of the ED & TC,
pp. 677-691, 1997.
[9] I. Hamzaoglu, et al., ”New Techniques for Deterministic Test Pattern Generation,” in
Proc. of VTS, pp. 446-452, 1998.
[10] J. Jain, et al., ”Probabilistic Design Verification,” in Proc. of ICCAD, pp. 468-471,
1991.
[11] J. Jain, et al., ”Formal Verification of Combinational Circuits,” in Proc. of Int. Conf.
on VLSI Design, pp. 218-225, 1997.
[12] S. K. Kumar, et al., ”Probabilistic Apects of Boolean Switching Functions via a New
Transform,” Journal of the ACM, pp. 502-520, July 1981.
[13] T. Kutzschebauch, et al., ”Congestion Aware Layout Driven Logic Synthesis,” in
Proc. of ICCAD, pp. 216-223, 2001.
[14] T. Larrabee, ”Test Pattern Generation Using Boolean Satisfiability,” IEEE Trans. on
Computer Aided-Design, pp. 4-15, Jan. 1992.
[15] S. Malik, et al., ”Logic Verification Using Binary Decision Diagrams in a Logic Synthesis
Environment,” in Proc. of ICCAD, pp. 6-9, 1988.
[16] K. P. Parker, et al., ”Probabilistic Treatment of General Combinational Networks,”
IEEE Trans. on Computer, pp. 668-670, June 1975.
[17] S. Reda, et al., ”Combinational equivalence checking using Boolean satisfiability and
binary decision diagrams,” in Proc. of DATE, pp. 122-126, 2001.
[18] E. M. Sentovich, et al., ”SIS: A System for Sequential Circuit Synthesis,” ERL Memo.
No.UCB/ERL M92/41, EECS, UC Berkeley, CA 94720.
[19] P. Stephan, et al., ”Combinational Test Generation Using Boolean Satisfiability,”
IEEE Trans. on Computer Aided-Design of Integrated Circuits and Systems, Vol. 15,
No. 9, Sept. 1996.
[20] M. Teslenko, et al., ”Computing a Perfect Input Assignment for Probabilistic Verification,”
in Proc. of SPIE, pp. 929-936, 2005.
[21] A. Veneris, et al., ”Logic Verification Based on Diagnosis Technique,” in Proc. of
ASPDAC, pp. 538-543, 2003.
[22] http://www.swox.com/gmp/

全文公開日期本全文未授權公開 (校內網路)
全文公開日期本全文未授權公開 (校外網路)

簡易檢索 / 詳目顯示

相關論文