實現高品質SoC設計之創新驗證與合成技術

Innovative Verification and Synthesis Techniques for Achieving High-Quality SoC Designs

周宏儒(Hong-Zu Chou)

指導教授 ： 郭斯彥

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

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

摘要

隨著系統單晶片設計（System-On-Chip，SoC）的發展，電路設計面臨的許多新的課題及挑戰，其中最為重大的挑戰就是如何確保一個複雜電路的功能正確性。大多數現存的驗證技術可以運作於暫存器傳輸層級（Register Transfer Level，RTL）與邏輯閘層級（Gate Level），為了盡早發現設計中的錯誤，驗證技術的發展趨勢逐漸朝向更高的設計抽象層級。在本論文中，我們針對系統單晶片在高階驗證所遇到的問題，提出許多創新的解決方案。首先，我們提出一個稱為BugHunter的基礎架構，該架構基於符號式模擬（Symbolic simulation）方法，整合許多優化技術，可改善高階驗證的效率及擴充性。

有鑑於高階符號式模擬的優點，在本論文中，我們開發了一個正規式程式碼可達性分析（Code-statement reachability analysis）技術。相對於傳統的覆蓋率分析方法，我們的技術可以準確地分析高階設計及測試平台的程式碼可達性，找出潛在的設計錯誤，大幅降低驗證所需的時間。然而，當任何程式碼被判斷為具有不可達性（Unreachability）時，由於可達性分析無法提供反例，分析錯誤的工作變得相當困難。針對這個問題，我們提出了一個不可達性診斷
（Unreachability diagnosis）技術，使用者可藉由這個技術快速地找出程式碼不可達性的原因，並加以修復。

除了功能性驗證問題之外，設計中的不確定性（Nondeterminism）問題逐漸在系統單晶片電路設計中的受到重視。設計中為了節省電力消耗或是解決繞線壅塞的問題，往往只將一些重要的暫存器接上重置信號。然而，未接上重置信號的暫存器可能會造成整體電路運作具有不確定性，導致嚴重的後果。針對這個問題，我們提出一個新穎的驗證機制，利用符號式模擬技術來找出大型電路中的不確定性問題。
此外，基於該驗證機制，我們也提出數個演算法來降低設計中需要重置信號的暫存器數量，以提昇系統單晶片設計的品質。

由於系統單晶片設計著重整合並重複利用已經存在的矽智產（Silicon Intellectual Properties），因此設計中可能存在相當多的無關項（Don't-cares）。例如對於一個只需要整數乘法的設計來說，其處理器中的浮點數運算單元可能永遠不會被使用到，如此便可將該浮點數運算單元視為一個無關項。在本論文中，我們利用上述的正規式程式碼可達性分析技術，找出設計中的無關項並且將其移除。實驗結果顯示，我們的方法能夠針對暫存器傳輸層級，移除不必要的程式碼，減少邏輯合成後的電路大小及降低電力消耗。
同時，我們的方法還可實現軟硬體共同設計及最佳化，對於系統單晶片設計有極大的幫助。

雖然大量的時間及人力被投入到驗證工作中，設計錯誤仍有可能到晶片下線後或是商品化後才被察覺。針對這個問題，我們提出了一個後矽錯誤修復（Post-silicon bug repair）機制，藉由產生軟體的限制規則（Constraints），達成硬體錯誤修復的目的。由於產生的限制規則可能相當複雜，不但造成軟體修改的困難，同時也降低系統的運作效率。因此，在本篇論文中，我們提出了新穎的最佳化技術，利用無關項來減少限制規則的大小及複雜度，在系統運作效率受到最小影響下，達成硬體修復的目的。

關鍵字

暫存器層級符號式模擬 ； 驗證 ； 系統不確定性驗證 ； 程式碼可達性分析 ； 不可達性診斷技術 ； 合成最佳化 ； 電路客製化

並列摘要

The increasing popularity of System-on-Chip (SoC) circuits results in many new design challenges. One major challenge is to ensure the functional correctness of such complicated circuits. While most existing verification techniques work well at the Register Transfer (RT) and gate levels, the growing trend is to extend verification to higher-level design abstractions in order to catch bugs early on. In this dissertation, we describe several innovative techniques to address the high-level verification problems for SoC designs. First, we propose a framework called BugHunter that consists of several enhancements and methodologies to improve the scalability and efficiency of high-level verification using symbolic simulation. To better leverage the power of high-level symbolic simulation, we develop a technique that can perform formal code-statement reachability analysis on designs and testbenches directly. This technique can detect bugs at high-level code directly, thus reducing verification time. Once unreachability is found, however, debugging is still an issue because the nature of unreachability prevents the
generation of counterexamples. To address this problem, we propose an innovative diagnosis technique that can identify root causes of unreachability.

In addition to functional verification, another issue that began to emerge in SoC circuits is the design nondeterminism problem. In order to save power or reduce routing congestion, a popular design methodology is to
reset important registers only. However, the uninitialized registers may cause nondeterminism in circuit behavior and cause serious problems. To catch such problems, we propose a nondeterminism verification technique using symbolic simulation and SAT solvers, and it can scale to large designs due to the accompanied novel methodology.
To further improve SoC quality, we also develop algorithms that can automate the reset register reduction process.

One major characteristic in SoC designs is the existence of abundant don't-cares. For example, the floating-point unit of a processor may never be used in a design that only requires integer multiplication. To utilize such don't-cares, we utilize our formal reachability analysis methods to identify and remove redundant code under the given input constraints. Our case studies show that this technique can remove unused RTL code and thus reducing the synthesized block area and power consumption. In addition, it can also
facilitate hardware/software co-design and co-optimization, a feature that is useful in early SoC design phases.

It has been pointed out that, although considerable effort
is applied to design verification, bug may still be undetected until tape-out or even the chip is commercialized, causing serious problems. To solve the problem, we propose a software-based post-silicon bug repair methodology that can automatically generate constraints for software so that hardware bugs can be worked around. Since the constraint may be complicated,
we also propose a novel optimization method based on don't-cares that can dramatically reduce the size of the constraint. In this way, software can be easily modified, either online or offline, so that it runs correctly on the buggy hardware.

並列關鍵字

RTL symbolic simulation ； verification ； X-verification ； code reachability analysis ； unreachability diagnosis ； synthesis optimization ； circuit customization

參考文獻

[3] Z. S. Andraus, M. H. Liffiton and K. A. Sakallah, “Refinement Strategies for Verification Methods Based on Datapath Abstraction,” Proc. Asia and South Pacific Design Automation Conference (ASPDAC), 2006, pp. 19-24.

[4] John Backes and Marc Riedel, “Reduction of Interpolants for Logic Synthesis,” Proc. International Workshop on Logic and Synthesis (IWLS), 2010.

[6] M. Benedetti, “sKizzo: A Suite to Evaluate and Certify QBFs,” Proc. International Conference on Automated Deduction (CADE), 2005, pp. 369-376

[7] V. Bertacco and M. Damiani, ”The Disjunctive Decomposition of Logic Functions,” Proc. International Conference on Computer Aided Design (ICCAD), 1997, pp. 78-82.

[8] V. Bertacco and K. Olukotun, “Efficient State Representation for Symbolic Simulation,” Proc. Design Automation Conference (DAC), 2002, pp. 99-104.