請用此 Handle URI 來引用此文件：
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/64525完整後設資料紀錄
| DC 欄位 | 值 | 語言 |
|---|---|---|
| dc.contributor.advisor | 江介宏 | |
| dc.contributor.author | Yi-Ting Chung | en |
| dc.contributor.author | 鍾逸亭 | zh_TW |
| dc.date.accessioned | 2021-06-16T17:52:26Z | - |
| dc.date.available | 2012-08-22 | |
| dc.date.copyright | 2012-08-22 | |
| dc.date.issued | 2012 | |
| dc.date.submitted | 2012-08-13 | |
| dc.identifier.citation | [1] P. Ashar and S. Malik. Functional timing analysis using ATPG. IEEE Trans. Comput.-Aided Design Integr. Circuits Syst., 14(8): 1025-1030, Aug. 1995.
[2] H.-C. Chen and D. Du. Path sensitization in critical path problem. IEEE Trans. Comput.-Aided Design Integr. Circuits Syst., 12(2): 196-207, Feb. 1993. [3] Y.-T. Chung and J.-H. R. Jiang. Functional timing analysis made fast and general. In Proc. Design Automation Conf., pp. 1055-1060, 2012. [4] O. Coudert. An e cient algorithm to verify generalized false paths. In Proc. Design Automation Conf., pp. 188-193, 2010. [5] S. Devadas, K. Keutzer, and S. Malik. Computation of oating mode delay in combinational circuits: Theory and algorithms. IEEE Trans. Comput.-Aided Design Integr. Circuits Syst., 12(12): 1913-1923, Dec. 1993. [6] M. Davis, G. Logemann, and D. Loveland. A machine program for theoremproving. Communications of the ACM, vol. 5, no. 7, pp. 394-397, 1962. [7] M. Davis and H. Putnam. A computing procedure for quanti cation theory. Journal of the Association for Computing Machinery, vol. 7, no. 3, pp. 201-215, 1960. [8] D.H. Du, S. H. Yen, S. Ghanta, On the General False Path Problem in Timing Analysis, Proc. 26th Design Automation Conf., 1989, pp. 555-560. [9] N. E en and N. S orensson. An extensible SAT-solver. In Proc. Int'l Conf. on Theory and Applications of Satis ability Testing, pp. 502-518, 2003. [10] Y.-M. Kuo, Y.-L. Chang, and S.-C. Chang. E cient Boolean characteristic function for timied automatic test pattern generation. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems, 28(3): 417-425, March 2009. [11] H. Kautz, E. Horvitz, Y.Ruan, C. Gomes, and B.Selman. Dynamic restart policies. In Proc. Eighteenth National Conf. on Arti cial Intelligence, pp. 674-382, 2002. [12] M. L. Littman, S. M. Majercik and T. Pitassi. Stochastic Boolean satis ability. Journal of Automated Reasoning, Vol. 27, No. 3, 251-296, 2001. [13] P. C. McGeer and R. K. Brayton. Integrating Functional and Temporal Domains in Logic Design. Kluwer Academic Publishers, 1991. [14] M. Moskewicz, C. Madigan, L. Zhang, and S. Malik. Cha : Engineering an efficient SAT solver. In Proc. Design Automation Conf., pp. 530-535, 2001. [15] J. Marques-Silva and K. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Trans. on Computers, vol. 48, no. 5, pp. 506-521, May 1999. [16] P. McGeer, A. Saldanha, R. Brayton, and A. Sangiovanni-Vincentelli. Delay Models and Exact Timing Analysis. In Logic Synthesis and Optimization, Kluwer Academic Publishers, pp. 167-189, 1993. [17] P. C. McGeer, A. Saldanha, P. R. Stephan, R. K. Brayton, and A. L. Sangiovanni-Vicentelli. Timing analysis and delay-fault test generation using path-recursive functions. In Proc. Int. Conf. on Computer-Aided Design, pages 180-183, 1991. [18] D. Plaisted and S. Greenbaum. A structure-preserving clause form translation. J. Symbolic Computation, 2:293-304, 1986. [19] S. Roy, P. P. Chakrabarti, and P. Dasgupta. Event propagation for accurate circuit delay calculation using SAT. ACM Trans. Design Autom. Electron. Syst., 12(3), Aug. 2007. [20] M. Riedel. Cyclic Combinational Circuits. Ph.D. thesis, California Institute of Technology, 2003. [21] L. Silva, J. Marques-Silva, L. Silveira, and K. Sakallah. Satis ability models and algorithms for circuit delay computation. ACM Trans. on Design Automation of Electronic Systems, 7(1): 137-158, Jan. 2002. [22] G. Tseitin. On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic, pp. 466-483, 1970. [23] Laung-Terng Wang, Yao-Wen Chang, and Kwang-Ting (Tim) Cheng. Electronic Design Automation, synthesis, veri cation, and test, 1st Edition. Feb 2009. | |
| dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/64525 | - |
| dc.description.abstract | 功能性時序分析跟結構性時序分析比起來，在電路延遲時間的計算上比較精確，但由於必須排除錯誤的關鍵路徑，其計算複雜度也會較高。雖然現今有很多演算法採用時間特徵函式(TCF)來將功能性時序分析問題轉化為布林可滿足性問題(SAT)，並運用一些技巧來加速求解，但這些演算法的效能與普遍性仍有待加強。
因此，在這篇論文中，我們發展了一套統一的時間特徵函式定義，讓它可以用來分析各式各樣的時序相關問題。此外，我們還提出了一種獨特的轉換方式，能非常有效率地將時間特徵函式轉換成連結正規形式(CNF)，以便用布林可滿足性求解器來求解。實驗數據顯示我們的演算法可以應用在業界規模的電路，並且解的比之前的方法快約十倍到千倍之多。 | zh_TW |
| dc.description.abstract | Functional, in contrast to structural, timing analysis for circuit delay computation is accurate, but computationally expensive in refuting false critical paths. Although satisfiability-based analysis using timed characteristic functions (TCFs) and modern satisfiability-solving techniques has been proposed, its efficiency and generality remain room for improvement.
This thesis provides a unified view on various TCFs for different timing requirements and a more efficient transformation from TCF formulas to conjunctive normal form (CNF) for satisfiability solving. Experimental results show functional timing analysis on industrial designs can be made up to several orders of magnitude faster and more generally applicable than prior methods. | en |
| dc.description.provenance | Made available in DSpace on 2021-06-16T17:52:26Z (GMT). No. of bitstreams: 1 ntu-101-R99943080-1.pdf: 757847 bytes, checksum: b231913a93acef9d8bd0ef7945eb019c (MD5) Previous issue date: 2012 | en |
| dc.description.tableofcontents | Acknowledgements i
Chinese Abstract ii Abstract iii List of Figures vii List of Tables viii 1 Introduction 1 1.1 Timing Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.1.1 Circuit Model . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.1.2 Static Timing Analysis . . . . . . . . . . . . . . . . . . . . . . 3 1.1.3 Functional Timing Analysis . . . . . . . . . . . . . . . . . . . 4 1.2 Satisability Problem . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.2.1 Conjunctive Normal Form . . . . . . . . . . . . . . . . . . . . 7 1.2.2 Circuit to CNF Conversion . . . . . . . . . . . . . . . . . . . . 7 1.2.3 Propositional Satisability . . . . . . . . . . . . . . . . . . . . 9 1.3 Thesis Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 1.3.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 1.3.2 Our Contribution . . . . . . . . . . . . . . . . . . . . . . . . . 11 1.3.3 Thesis Organization . . . . . . . . . . . . . . . . . . . . . . . 12 2 Related Work 13 2.1 Denition of TCF . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.2 Satisability of Timing Requirement . . . . . . . . . . . . . . . . . . 14 2.3 Formulation of TCF . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.3.1 TCF without 0/1-Specicity . . . . . . . . . . . . . . . . . . . 14 2.3.2 TCF with 0/1-Specicity . . . . . . . . . . . . . . . . . . . . . 16 2.4 Reduction Techniques . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 3 Ecient TCF Formulation for Various Applications 18 3.1 Maximum Delay Computation . . . . . . . . . . . . . . . . . . . . . . 19 3.1.1 TCF without 0/1-Specicity . . . . . . . . . . . . . . . . . . . 20 3.1.2 TCF with 0/1-Specicity . . . . . . . . . . . . . . . . . . . . . 24 3.2 Minimum Delay Computation . . . . . . . . . . . . . . . . . . . . . . 27 3.2.1 TCF without 0/1-Specicity . . . . . . . . . . . . . . . . . . . 28 3.2.2 TCF with 0/1-Specicity . . . . . . . . . . . . . . . . . . . . . 29 3.3 Cyclic-Circuit Delay Computation . . . . . . . . . . . . . . . . . . . . 29 3.4 Comparison on TCF Formulas . . . . . . . . . . . . . . . . . . . . . . 30 4 Our Reduction Techniques 33 4.1 Equivalence Table . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 4.1.1 0/1-Specied Arrival Times . . . . . . . . . . . . . . . . . . . 34 4.1.2 Constant Boundary Conditions . . . . . . . . . . . . . . . . . 34 4.1.3 Applicable for PIs/POs . . . . . . . . . . . . . . . . . . . . . . 35 4.2 Arrival Time List Computation . . . . . . . . . . . . . . . . . . . . . 35 4.2.1 Combinational Circuit . . . . . . . . . . . . . . . . . . . . . . 36 4.2.2 Cyclic Combinational Circuit . . . . . . . . . . . . . . . . . . 37 4.2.3 Refute False Arrival Times . . . . . . . . . . . . . . . . . . . . 38 4.3 Variable Indexing of CNF . . . . . . . . . . . . . . . . . . . . . . . . 40 5 Algorithm 42 5.1 Delay Computation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 5.2 Critical Region Identication . . . . . . . . . . . . . . . . . . . . . . . 43 6 Experimental results 45 6.1 Maximum Delay Computation . . . . . . . . . . . . . . . . . . . . . . 45 6.2 Critical Region Identication . . . . . . . . . . . . . . . . . . . . . . . 53 7 Conclusions and Future Work 54 Bibliography 55 | |
| dc.language.iso | en | |
| dc.subject | 時間特徵函式 | zh_TW |
| dc.subject | 時序分析 | zh_TW |
| dc.subject | 布林可滿足性求解 | zh_TW |
| dc.subject | 錯誤路徑 | zh_TW |
| dc.subject | false path | en |
| dc.subject | satisfiability solving | en |
| dc.subject | timed characteristic function | en |
| dc.subject | timing analysis | en |
| dc.title | 以簡化之時間特徵函式加速功能性時序分析之方法 | zh_TW |
| dc.title | Accelerating Functional Timing Analysis with Simplfied Timed Characteristic Functions | en |
| dc.type | Thesis | |
| dc.date.schoolyear | 100-2 | |
| dc.description.degree | 碩士 | |
| dc.contributor.oralexamcommittee | 王凡,江蕙如,陳郁方,王俊堯 | |
| dc.subject.keyword | 錯誤路徑,布林可滿足性求解,時間特徵函式,時序分析, | zh_TW |
| dc.subject.keyword | false path,satisfiability solving,timed characteristic function,timing analysis, | en |
| dc.relation.page | 56 | |
| dc.rights.note | 有償授權 | |
| dc.date.accepted | 2012-08-13 | |
| dc.contributor.author-college | 電機資訊學院 | zh_TW |
| dc.contributor.author-dept | 電子工程學研究所 | zh_TW |
| 顯示於系所單位： | 電子工程學研究所 | |
文件中的檔案：
| 檔案 | 大小 | 格式 | |
|---|---|---|---|
| ntu-101-1.pdf 未授權公開取用 | 740.08 kB | Adobe PDF |
系統中的文件，除了特別指名其著作權條款之外，均受到著作權保護，並且保留所有的權利。