以簡化之時間特徵函式加速功能性時序分析之方法

Accelerating Functional Timing Analysis with Simplfied Timed Characteristic Functions

鍾逸亭(Yi-Ting Chung)

指導教授 ： 江介宏

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

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

摘要

功能性時序分析跟結構性時序分析比起來，在電路延遲時間的計算上比較精確，但由於必須排除錯誤的關鍵路徑，其計算複雜度也會較高。雖然現今有很多演算法採用時間特徵函式(TCF)來將功能性時序分析問題轉化為布林可滿足性問題(SAT)，並運用一些技巧來加速求解，但這些演算法的效能與普遍性仍有待加強。

因此，在這篇論文中，我們發展了一套統一的時間特徵函式定義，讓它可以用來分析各式各樣的時序相關問題。此外，我們還提出了一種獨特的轉換方式，能非常有效率地將時間特徵函式轉換成連結正規形式(CNF)，以便用布林可滿足性求解器來求解。實驗數據顯示我們的演算法可以應用在業界規模的電路，並且解的比之前的方法快約十倍到千倍之多。

關鍵字

錯誤路徑 ； 布林可滿足性求解 ； 時間特徵函式 ； 時序分析

並列摘要

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.

並列關鍵字

false path ； satisfiability solving ； timed characteristic function ； timing analysis

參考文獻

[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.

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.