功能性時序分析方法FUNCTIONAL TIMING ANALYSIS METHOD FOR CIRCUIT TIMING VERIFICATION

專利類型

發明

專利國別 (專利申請國家)

美國

專利申請案號

13/672,760

專利證號

US 8,671,375 B1

專利獲證名稱

功能性時序分析方法FUNCTIONAL TIMING ANALYSIS METHOD FOR CIRCUIT TIMING VERIFICATION

專利所屬機關 (申請機關)

國立臺灣大學

獲證日期

2014/03/11

技術說明

電路的時序分析在驗證領域有很大的用途。其中功能性時序分析跟結構性時序 分析比起來，在電路延遲時間的計算上比較精確，但由於必須排除錯誤的關鍵 路徑，其計算複雜度也會較高。雖然現今有很多演算法採用時間特徵函式(Timed Characteristic Function, TCF)來將功能性時序分析問題轉化為布林可滿足性問題 (Satisfiability, SAT)，並運用一些技巧來加速求解，但這些演算法並無法解決太 大規模的問題。因此我們提出了一種獨特的轉換方式，能非常有效率地將時間特徵函式 轉換成連結正規形式(Conjunctive Normal Form)，以便用布林可滿足性求解器來 求解。實驗數據顯示我們的演算法可以應用在業界規模的電路，並且解的比之 前的方法快。 本發明提供了一種功能的時序分析方法，在計算設備中執行的方法，包括：步驟A：獲得電路;步驟B：選擇從電路中的一個節點設定一個延遲時間;步驟C：產生與該節點所選擇的延遲時間相關聯的時序特徵函數產生作為目標公式;步驟D：透過使用蘊涵算子遞迴地將所述時序特徵函數轉換為目標公式的時序特徵函數條件;步驟E中：使用布林求解器檢查目標公式是否被滿足，以及步驟F：如果目標式可被滿足，輸出所選擇的最大延遲時間。 A functional timing analysis method, executed in a computing device, comprises: step A: obtaining a circuit; step B: selecting a target delay time from a delay time set for a node in the circuit for verifying whether the target delay time is attainable by some input assignment; step C: generating a timed characteristic function associated with the selected target delay time for the node recursively from the timed characteristic functions associated with the corresponding delay times for its fanin nodes is generated as a target formula; step D: recursively translating the timed characteristic function into timed characteristic function clauses of the target formula by using an implication operator; step E: checking whether the target formula is satisfied by using a Boolean satisfiability solver; and step F: if the target formula is satisfied, the selected target delay time is attainable by some input assignment to the circuit.

備註

連絡單位 (專責單位/部門名稱)

產學合作總中心

連絡電話

33669945

網址