驗證意識之超大型積體電路邏輯最佳化技術之研究

On Synthesis and Optimization of VLSI Designs for Verification

陳勇志(Yung-Chih Chen)

指導教授 ： 王俊堯

國立清華大學/電機資訊學院/資訊工程學系/博士(2011年)

https://doi.org/10.6843/NTHU.2011.00490

摘要

隨著設計複雜度增加，驗證(verification)已成為電路設計過程中的主要瓶頸之一。研究顯示，驗證可能花費整體電路開發過程的40%~70%的時間。因此，若能有效地加速驗證將可以直接地減少電路開發所花費的時間。在本論文中，我們提出三個邏輯最佳化技術以加速電路驗證程序。
首先，對於以模擬為基礎的驗證程序，我們提出一個可以簡化限制電路(constraint circuit)的技術。限制電路乃是用於產生合法輸入值給欲驗證的電路(design under verification)。對於限制電路，我們關注的是其所會產生的所有輸出組合(output range)，而非其功能(functionality)。而我們所提出的技術則可以在不改變限制電路的所有輸出組合條件下簡化之(減少輸入與邏輯閘數量)。簡化後的限制電路，可以在相同的運算時間內產生更多不同的合法輸入值，因此可以加速驗證。
接著，對於以滿足性(satisfiability)為基礎的等效驗證方法，我們提出兩個改變電路架構並簡化電路的技術。首先，我們研究合併電路中兩節點的技術，也就是使用電路中的一節點去取代另一節點。因為，被取代的節點可以被移除而不改變電路的功能，所以此技術可以簡化電路並改變電路架構。接著，我們延伸此節點合併技術，透過加入一節點已取代欲移除的節點。當加入的節點數比移除的節點數少時，此技術一樣可以簡化電路並改變電路架構。我們所提出的方法比過去的技術更有效率，而同時具有相當的電路簡化能力。最後，我們將此兩技術應用於以滿足性為基礎的等效驗證，透用簡化電路並改變電路架構以降低驗證複雜度，而加速驗證時間。結果顯示，我們對於所使用的所有測試電路，總共可以省下27小時的驗證時間。

關鍵字

超大型積體電路 ； 設計自動化 ； 電腦輔助設計 ； 電路驗證 ； 電路最佳化

並列摘要

With the growth of design complexity, verification has become one of the primary bottlenecks of the design process. Studies show that verification could take 40% to 70% of the total development effort for the design. As a result, reducing verification time directly affects the design cycle. In this dissertation, we propose three logic optimization methods to facilitate verification process.

We first focus on simulation-based functional verification. A range-equivalent circuit optimization method is proposed to minimize a constraint circuit that is responsible for generating legal input patterns for a design under verification. This method could minimize a constraint circuit while preserving its range such that the pattern generation process could be accelerated and the patterns remain legal. The experimental results show that the proposed method can minimize a benchmark with an average of 37.06% reduction in terms of the number of primary inputs, and an average of 36.31% reduction in terms of the number of nodes. Additionally, each simplified benchmark can generate more output combinations than the non-simplified one for the same random simulation time.

Next, we focus on satisfiability (SAT)-based equivalence checking. A node-merging method is proposed to merge two nodes (use one node replace another node) in a circuit which are functional equivalent or their functional differences are never observed at any primary output. When two nodes are merged, one of them can be removed from the circuit, and this merger may cause other redundancies in the circuit such that the resultant circuit is minimized. The experimental results show that the proposed method is 46 times faster than a previous method and has a competitive capability of circuit size reduction. Furthermore, a node addition and removal (NAR) method is proposed to enhance the node-merging method. It creates a node merger by adding a node into the circuit. When more than one node is removed due to the addition of the new node, the circuit size is reduced as well. The experimental results show that the optimization capability of the NAR method is better than that of the proposed node-merging method with a ratio of 1.27. The overall CPU time overhead is only 242.8 seconds. We further apply these two methods to facilitate bounded sequential equivalence checking. A total of approximately 27-hour verification time is saved for all the benchmarks.

並列關鍵字

Very-large-scale integration ； Electronic design automation ； Computer-aided design ； Design verification ； Logic optimization

參考文獻

[2] M. Abramovici, M. A. Breuer, and A. D. Friedman, Digital Systems Testing and Design for Testability, IEEE Press, 1990.

[5] J. Baumgartner and H. Mony, “Maximal Input Reduction of Sequential Netlists via Synergistic Reparameterization and Localization Strategies," in Proc. Int. Conf. on Correct Hardware Design and Verification Methods, 2005, pp. 222-237.

[6] Berkeley Logic Synthesis and Verification Group, “ABC: A System for Sequential Synthesis and Verification," http://www.eecs.berkeley.edu/~alanmi/abc/.

[7] C. L. Berman and L. H. Trevillyan, “Functional Comparison of Logic Designs for VLSI Circuits," in Proc. Int. Conf. on Computer-Aided Design, 1989, pp. 456-459.

[8] A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu, “Symbolic Model Checking Using SAT Procedures instead of BDDs," in Proc. Design Automation Conf., 1999, pp. 317-320.