運用設計自動抽象化技術增進限制隨機向量生成效能

Improving Constrained Random Pattern Generation by Automatic Design Abstraction

張靖宗(Ching-Zong Chang)

指導教授 ： 黃鐘揚

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

https://doi.org/10.6342/NTU202204156

摘要

隨著積體電路規模與複雜度的增長，功能驗證在晶片設計流程中的重要性日增。基於模擬的約束隨機驗證方法，因能有效處理複雜度指數成長的大規模晶片設計，而成為業界的主流驗證方式。但其追求高生成率與均勻分布的特性，使測試向量在策略性與目的性上都有所不足，模擬器只能在設計狀態空間中以隨機遊走的方式進行探索。本研究提出設計抽象化技術提供晶片設計與反例的宏觀全局結構模型，再結合精緻化技術來有系統性的補充與驗證目標有關的必要設計細節。據此指引生成器有目的性的生成測試向量。在大規模數位系統的實驗結果顯示，我們的方法在驗證安全屬性的能力、速度與給出的反例質量上都明顯優於原始方法。

關鍵字

功能性測試 ； 限制隨機驗證 ； 抽象化與精細化

並列摘要

With the rapid growth in the scale and complexity of integrated circuits, functional verification has become increasingly important in the IC design flow. Simulation-based Constrained random methods can effectively handle the exponential growth of large-scale designs. Therefore, it has become the mainstream verification method in the industry. However, its high throughput and uniform distribution in probability make the generated patterns unplanned and meaningless. The simulator can only explore the design state space by random walk. This thesis proposes a design abstraction technique to provide an abstract model of the design and counterexamples, combined with refinement techniques to systematically supplement it with the necessary details related to the verification goals. This "big picture" model guides the generator to produce more purposeful patterns. Experimental results on large-scale digital systems show that our method significantly outperforms the original approach in runtime, verification ability, and quality of counterexamples.

並列關鍵字

Functional Verification ； Constrained Random Verification ； Abstraction and Refinement

參考文獻

[1] L. Devroye, "Random variate generation for unimodal and monotone densities," Computing, vol. 32, no. 1, pp. 43–68, Mar. 1984.

[2] J. Yuan, A. Aziz, C. Pixley, and K. Albin, "Simplifying Boolean Constraint Solving for Random Simulation-Vector Generation," IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 23, no. 3, pp. 412–420, Mar. 2004.

[3] N. Kitchen and A. Kuehlmann, "A Markov Chain Monte Carlo Sampler for Mixed Boolean/Integer Constraints," in Computer Aided Verification. pp. 446–461, Springer. 2009.

[4] S. M. Plaza, I. L. Markov, and V. Bertacco, "Random stimulus generation using entropy and XOR constraints," in the conference, Munich, Germany, Mar. 10–14, 2008.

[5] Shujun Deng, Zhiqiu Kong, Jinian Bian, and Yanni Zhao, "Self-adjusting constrained random stimulus generation using splitting evenness evaluation and XOR constraints," in 2009 Asia and South Pacific Design Automation Conference (ASP-DAC), Yokohama, Japan, Jan. 19–22, 2009.