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

Abstract

功能性時序分析跟結構性時序分析比起來，在電路延遲時間的計算上比較精確，但由於必須排除錯誤的關鍵路徑，其計算複雜度也會較高。雖然現今有很多演算法採用時間特徵函式(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.