針對複雜數位設計上功能驗證的電腦輔助技術之研究

Abstract

由於現今的電路設計越來越複雜，驗證電路的正確性已經慢慢成為整個設計流程當中最主要的瓶頸。到目前為止，在暫存器轉移層次(RTL)上用來驗證以硬體描述語言(HDL)寫成之電路功能的方法主要有兩種，一種是軟體模擬(simulation)，一種是正規驗證(formal verification)，但是這兩種方式在設計的複雜度越來越高時都會面臨相當大的瓶頸。軟體模擬所遭遇到的主要問題是，它缺乏一個很好的標準去評斷測試的完整性，這往往造成需要很龐大的測試向量來測試複雜的設計。而正規驗證的方式雖然沒有這種完整性的問題，但是它在處理較大電路時，卻常常遭遇到運算資源不足的限制。 因此，一種結合了軟體模擬與正規驗證兩者優點的所謂”涵蓋率驅動” (coverage-driven)的方式被提出來解決這個問題，並且很快的廣為大家所接受。在這種方式裡，我們使用一些已經清楚定義的涵蓋率量度(coverage metrics)來評斷模擬的完整性，有了這些涵蓋率報告之後，我們就可以把精神放在尚未測試到的部分，運用正規驗證的技術或是設計者本身對電路的了解，針對這些地方產生更多測試向量，以達到更好的功能涵蓋率。雖然以目前的技術來說，百分之百的涵蓋率仍然沒辦法保證這個電路是百分之百沒有錯誤，但是它至少提供了一種較為系統化的方式來評估驗證的完整性，使得我們能夠更加提升驗證的效率。 在這篇論文中，我們針對這種以涵蓋率為基礎來解決功能驗證問題的方式做了一個完整的研究，並試著提出一些改進的方法來處理複雜的電路。在眾多的涵蓋率量度之中，我們選擇最廣泛也最完整的有限狀態機(FSM)涵蓋率來當作整個流程中的目標，但是由於現今電路的複雜度太高，其狀態轉換圖(STG)常常大到無法全部驗證完畢，因此我們提出了一種改良的有限狀態機涵蓋率：語意有限狀態機(semantic FSM)涵蓋率，藉由分析設計的描述語法，將需要被測試的狀態轉換圖縮減至可接受的大小，來解決複雜度太高的問題。 為了處理現今設計中的龐大複雜度，一種可能的方法是使用設計抽象化(abstraction)的技術先把問題簡化。在設計的初期，大部份的設計錯誤都發生在控制器的部份，如果我們可以把資料流(datapath)的部份分離開來，只驗證控制邏輯的部份，問題的複雜度就可以有效地被簡化。因此，我們提出了一個自動化的控制器淬取技術，它能夠自動地從硬體描述中把設計裡的有限狀態機分離出來，並在這些有限狀態機之中挑選最合適的部分來當作需要被驗證的控制邏輯。由於我們的技術並非根據事先定義好的語法去辨認，而是根據有限狀態機裡現在狀態(current state)與下一個狀態(next state)之間的關係來著手，因此我們幾乎不需對使用者的寫法作任何的限制，也不需要使用者在他的描述裡加入任何的提示。 當設計裡的有限狀態機被分離出來之後，我們就可以很容易的在模擬過程中觀察它們的有限狀態機涵蓋率以及語意有限狀態機涵蓋率。在這個涵蓋率量測的步驟上，我們提出了一種新的方法，能夠從模擬器產生的數值改變紀錄檔(value change dump file)中去分析這次模擬的涵蓋率。由於這種方式是在模擬完之後才做涵蓋率分析，因此可以在分析速度相去不遠的前提之下，讓整個使用流程變得比現有的工具更為簡單而平順，而且大大地增加了選擇不同的涵蓋率量度及測量區域的彈性。 在量測模擬的涵蓋率之後，我們也許需要針對未測試到的狀態轉換(state transition)產生更多的測試向量，所以我們提出了一個自動測試向量產生器的核心技術，藉由前面所提出的有限狀態機淬取技術，很合理的將整個大電路分割成一些較小的有限狀態機，然後，只要運用各個擊破的策略，一個一個來處理這些小電路，就能夠大大地降低記憶體的需求，克服傳統符號運算技術(symbolic technique)裡處理較大電路時遇到的記憶體容量問題。 除了以上這些技術之外，我們另外還提出了一個輔助性的技術，可以協助使用者縮短驗證的時間。在製造測試的應用中，可測試性設計(design-for-testability)的技術是一項廣為人知可以用來減少測試時間的方法，因此，我們也把類似的想法應用到功能驗證的領域中，提出了一個有效率的可驗證性設計(design-for-verification)技術，可以在不降低驗證品質的前提下，大大地減少驗證所需的功能測試向量。

Due to the increasing design complexity, verification is now the major bottleneck of the entire design process. In order to verify the functionality of the initial register-transfer level (RTL) designs written in hardware description language (HDL), two primary approaches, simulation and formal verification, are often used. However, both techniques encounter some difficulties in dealing with the increasing circuit complexity. The major problem of the simulation-based approaches is the lack of metrics to gauge the quality of the test, which often results in the huge amount of test benches for complex designs. Although formal verification techniques can solve the quality concern in the simulation-based approaches, they are often limited by the computation resources in dealing with large circuits. Therefore, the coverage-driven approach, which combines the ideas of simulation and formal verification, is proposed and rapidly getting popular. Some well-defined functional coverage metrics are used in this approach to perform a quantitative analysis of simulation completeness. With the coverage reports, the verification engineers can focus their efforts on the untested areas and generate more patterns by the help of formal techniques or the designers’ knowledge to achieve better functional coverage. Although 100% coverage still cannot guarantee a 100% error-free design, it provides a more systematic way to measure the completeness of the verification process such that the productivity can be greatly improved. In this dissertation, we study the entire flow of the coverage-driven approach for functional verification problem and try to propose some improvements to handle complex designs. Among the various functional coverage metrics, we choose the most general and complete metric, finite state machine (FSM) coverage, to be the target metric for the entire flow. Because the sizes of the state transition graphs (STGs) for modern designs are often too large to be traversed completely, we propose an improved FSM coverage metric, semantic finite state machine (SFSM) coverage, to reduce the tested STGs to acceptable sizes by using the content of HDL code. In order to deal with the huge state space in modern designs, one possible solution is to use abstraction techniques. In early design stage, most design errors are related to the control part of the design. If we can separate the datapaths from the controllers and verify the control part only, we can effectively reduce the problem size. For this purpose, we propose an automatic controller extractor that can extract FSMs automatically from the HDL descriptions and then select suitable FSMs to be the verified control part. Because we use the relationship between the current states and the next states of a FSM instead of the predefined language constructs for the extraction, there are almost no restrictions on the writing style of HDL codes. No hints or comments in the source codes are needed, either. After the FSMs are extracted from the HDL descriptions, we can easily analyze their FSM coverage and SFSM coverage during simulation. For coverage analysis, we propose a novel approach for functional coverage measurement based on the value change dump (VCD) files produced by the simulators. Because we analyze the functional coverage by post-processing, the usage flow of our approach is much easier and smoother than that of existing instrumentation-based coverage tools. The flexibility in choosing different coverage metrics and measured code regions could be easily increased with competitive performance. For the uncovered state transitions reported in the coverage analysis step, we may have to generate more test bench to traverse those transitions. Therefore, we propose an automatic test bench generation engine that can overcome the memory issues in the symbolic techniques. According to the results of the proposed FSM extraction techniques, we can reasonably partition the HDL designs into some small FSMs. By using the “divide and conquer” strategy for those small FSMs, the peak memory requirement could be significantly reduced to handle large cases. Besides those techniques mentioned above, we also propose an assistant technique to help users reduce the verification time. In manufacturing test, a well-known technique, “design-for-testability” (DFT), is often used to reduce the testing time. Therefore, we applied the similar idea to functional verification and proposed an efficient “design-for-verification” (DFV) technique. By the help of this technique, we can greatly reduce the number of required functional patterns without any loss on the verification quality.