利用強健的全域與區域之無解空間辨識技術來提升限制性隨機樣本產生效能

Improving Constrained Random Pattern Generation by Powerful Global and Local Infeasible Solution Space Identification

林恩祥(En-Hsiang Lin)

指導教授 ： 黃鐘揚

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

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

摘要

功能性驗證在晶片設計流程上是不可或缺的一環。其中，直接測試是工業上最被廣泛使用的方法。它能在驗證初期快速檢驗電路基本功能。然而，其所產生的測試向量容易受限於使用者對待測系統的認知而產生分布不均的現象，使得一些角落錯誤不易觸發，進而影響到待測電路的測試覆蓋率。另一類被稱為限制式随機驗證的方法在近年來受到了重視。使用者只需根據待測電路規格與驗證的目標撰寫輸入限制式。接著，限制式求解器會自動產生大量滿足輸入限制式的測試向量。與直接測試的方法相比，它能快速並有效的產生更多的測試向量來模擬待測電路。
限制式求解技術是整個隨機驗證方法的核心。一個好的限制式求解器應該包含以下性質：1) 高生產率 2) 均勻分布(機率上) 3) 均勻分布(空間上)。換言之，它應該要能有效率的快速產生測試向量，並且同時保證產生的測試向量在機率和解空間角度上是均勻分散的。本篇論文針對一些較為困難的例子去提高測試向量的產生速率。我們的改進主是要建立在辨識更多的無解空間。當無解空間能辨識愈多，限制式求解器效率也會進一步提高。
我們把辨識流程分為兩階段：1) 全域無解空間辨識 2) 區域無解空間辨識。 兩者適用在不同的情況。在全域無解空間辨識的階段中，它過濾了包含有可全域式縮減變數的無解空間。一個變數如果初始範圍可以在不考慮其他變數的賦值下進行縮減，該變數稱為可全域式縮減變數。我們提出了一個迭代事件驅動的方法搭配正規詞級解法器去辨識出該類型變數。在區域無解空間辨識的階段，剩下的無解空間大部份是由可條件式縮減的變數所組成。一個變數如果需在同時考慮部份其他變數的數值情況下才能進行縮減，稱為可條件式縮減變數。我們使用了既有文獻裡所提出的範圍切割樹方法來過濾該類型的無解空間。範圍切割樹的樣式顯著地影響了無解空間辨識的能力。我們建置範圍切割樹的方法是去動態地選擇當下最困難的一條限制式做切割。實驗結果顯示，這種以貪心為基礎的建置方法能更有效地辨識出無解空間因此測試向量的生產率能因此大幅提高。

關鍵字

功能性測試 ； 限制式隨機驗證 ； 範圍切割樹

並列摘要

Functional verification is indispensable in circuit design flow. Directed testing is the most prevalently used method in industry. It can quickly validate basic functionality of design under verification (DUV) at the early stage. However, the generated test vectors are easily biased due to the designers’ perception on the DUV, which lowers the chance to trigger corner bugs. This greatly affects the test coverage of DUV. Another approach called Constraint Random Verification (CRV) draws more attention in recent years. Users provide input constraints based on system specification and their intention for verification, and then a constraint solver would efficiently generate vast amounts of patterns that satisfy the constraints. Compared to former approach, it can quickly generate more effective patterns to simulate the DUV.
Constraint solving technique is the key of CRV methodology. A good constraint solver for CRV should have the following properties: 1) high throughput 2) uniform distribution (in probability) 3) high pattern diversity (in search space). In other words, it should efficiently generate valid patterns while ensuring evenness and pattern diversity at the same time. In this thesis, we focus on improving throughput for some rather difficult cases. Our improvements mainly come from the identification of infeasible solution space for the input constraints. Intuitively, as more infeasible solution space is identified, the higher throughput the constraint solver can be achieved.
We divide the identification into two stages: 1) global infeasible space identification 2) local infeasible space identification. They apply to different situations. At global infeasible space identification stage, it filters out infeasible space which consists of universally reducible variables. A variable is universally reducible if its initial range can be reduced without consideration of the assignments of other variables. We proposed an iterative event-driven approach combined with the word-level SMT solver to identify such space. At local infeasible space identification stage, remaining infeasible space is mostly composed of conditionally reducible variables. A variable is conditionally reducible if its range can only be reduced with regard to the assignments of some of other variables. We utilize the Range Splitting Tree (RST) technique to filter out such infeasible space. The structure of constructed RST greatly affects the ability of infeasible space identification. Our RST construction is guided by dynamically selecting the constraint with lowest hit rate on-the-fly. Experimental results show the effectiveness of this greedy based construction to identify infeasible space, and thus the throughput can be substantially enhanced.

並列關鍵字

Functional Verification ； Constrained Random Verification ； Range Splitting Tree

參考文獻

[1] SystemVerilog LRM can be found at http://www.systemverilog.org.

[3] S. Deng, Z. Kong, J. Bian and Y. Zhao, "Self-Adjusting Constrained Random Stimulus Generation Using Splitting Evenness Evaluation and XOR Constraints," Asia and South Pacific Design Automation Conference (ASPDAC), 2009.

[4] B.-H. Wu, C.-J. Yang, C.-C. Tso and C.-Y. (Ric) Huang, “Toward an Extremely-High-Throughput and Even-Distribution Pattern Generator for the Constrained Random Simulation Techniques,” International Conference on Computer-Aided Design (ICCAD), pp. 602-607, 2011.

[5] L. Devroye, "Random Variate Generation for Unimodal and Monotone densities," Computing, pp.43-68, 1984

[6] J. Yuan, A. Aziz, C. Pixley, and K. Albin, “Simplifying Boolean Constraint Solving for Random Simulation-Vector Generation,” IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, pp. 412-420, 2004.