針對偵測及診斷設計錯誤之演算法之研究

Abstract

由於現今的特殊用途晶片（ASIC）以及系統單晶片（SoC）的電路設計日趨複雜，功能驗証（Functional Verification）占據了產品發展的大部分時間。以Assertion為基礎的驗証（Assertion-based Verification, ABV）能夠較傳統的技術更快地幫助設計團隊找出以及除去設計錯誤（Design Error）。藉由在電路設計中嵌入Assertion且同時觀察電路的行為，ABV能夠比對並找出電路設計的實作和所描述的Assertion之間的異同。因此，ABV已被視為在設計驗証流程中最重要的一項利器。 一般來說，偵測以及診斷設計錯誤扮演了ABV流程中最重要的角色。不幸的是，從前所提出之錯誤偵測的技巧無法跟上設計複雜度的快速增加。此外，由ABV產生的錯誤軌跡（Error Trace）常常太冗長使得診斷反例（Counterexample）的工作變得非常煩燥且困難。在本論文中，我們針對如何更有效率地偵測設計錯誤，以及如何減輕除錯的過程提出了三種演算法。 首先，我們提出了能指引有界模型檢查（Bounded Model Checking, BMC）的界限計算（Cycle Bound Calculation）演算法。BMC已被公認為偵測設計錯誤最有效的技術之一；然而，BMC的缺點在於，它需要一事先計算好的界限以確保其完整性。為了能幫助BMC決定此一界限，我們提出了採用分支及劃界（Branch and Bound）的演算法。在此演算法中，我們藉由分割（Partitioning）及修剪（Pruning）的技術來降低電路設計中所要搜尋的空間。此外，我們提出了一創新公式並利用SAT解答器（SAT-solver）來找出BMC所需之界限。實驗結果証明，相較於從前的技術，我們的方法大大地提高界限計算的準確度。 接著，為了進一步找出一些相當難以偵測的設計錯誤，我們提出了一半正規驗証（Semi-formal Verification）的演算法。在實際的工業界環境中，半正規驗証結合了模擬及正規的技術以對付棘手的驗証問題。然而，單調而無變化地結合這些異質技術使得半正規驗証無法跟上電路設計複雜度的高速成長。因此，我們提出了利用個個擊破（Divide and Conquer）技巧的演算法來精心安排及協調這些異質技術。我們提出一分割技巧使得複雜的電路可以被遞迴地分解成小的成分。此外，我們還提出分別處理各個小成分且保存電路功能完整性的方法。實驗結果証明，我們的演算法確實能偵測出過去半正規驗証方法所無法找出的設計錯誤。 最後，為了使設計錯誤的診斷更加容易，我們提出了錯誤軌跡壓縮方法。一般而言，用來追蹤及觀察電路設計行為的錯誤軌跡，其長度通常非常冗長；這使得電路設計工程師需要花費很可觀的精力去了解它們。為了減輕工程師們的負擔，我們利用SAT解答器發展了一套降低錯誤軌跡長度的最佳演算法。此演算法不但能遞迴式地將電路的搜尋空間減半，而且能保証所得的長度為最短。基於此最佳演算法，我們額外提出了兩種策略以應付實際電路。實驗結果指出，我們所提出的技術遠勝過前人所提出的方法，且我們所得的結果確實能被實際運用於工業界上。

Functional verification now accounts for most of the time spent in the product development due to the increasing complexity of modern ASIC and SoC designs. Assertion based verification (ABV) helps design teams identify and debug design errors more quickly than traditional techniques. It compares the implementation of a design against its specified assertions by embedding assertions in a design and having them monitor design activities. As a result, ABV is recognized as a critical component of the design verification process. In general, detecting and diagnosing design errors play the most important role in ABV. Unfortunately, the proposed techniques for design error detection cannot keep up with the rapid growth of design complexity. Furthermore, the generated error traces are usually very lengthy such that diagnosing counterexamples becomes very tedious and difficult. In this dissertation, we focus on three strategies that address the problem of efficiently detecting design errors and easing debug process. We first propose a practical cycle bound calculation algorithm for guiding bounded model checking (BMC). Many reports have shown the effectiveness of BMC in design error detection; however, the flaw of BMC is that it needs a pre-computed bound to ensure completeness. To determine the bound, we develop a practical ap-proach that takes branch-and-bound manner. We reduce the search space by applying a partitioning as well as a pruning method. Furthermore, we propose a novel formula-tion and use the SAT-solver to search states and thus determine the cycle bound. Ex-perimental results show that our algorithm considerably enhances the performance compared with the results of the previous work. We then propose an advanced semi-formal verification algorithm for identifying hard-to-detect design errors. Generally, semi-formal verification combines the simula-tive and formal methods to tackle the tough verification problems in a real industrial environment. Nevertheless, the monotonous cooperation of the heterogeneous meth-ods cannot keep pace with the rapid growth of design complexity. Therefore, we pro-pose an elegant algorithm that takes divide-and-conquer paradigm to orchestrate those approaches. We introduce a partitioning technique to recursively divide a design into smaller-sized components. Moreover, we present the approaches of handling each divided component efficiently while keeping the entire design function correct. Ex-perimental results demonstrate that our strategy indeed detects much more design errors than the traditional methods do. At last, we propose powerful error trace compaction algorithms to ease design error diagnosis. Usually, the error traces used to exercise and observe design behavior are very lengthy such that designers need to spend considerable effort to understand them. To alleviate designers’ burden, we present a SAT-based algorithm for reducing the lengths of the error traces. The algorithm not only halves the search space recur-sively but also guarantees to acquire the shortest lengths. Based on the optimum algo-rithm, we also develop two robust heuristics to handle real designs. Experimental results indicate that our approaches greatly surpass previous work and certainly give the promising results.