智慧型驗證之高階設計資訊箤取技術

High-Level Design Intent Extraction for Intelligent Verification

張啟文(Chi-Wen Chang)

指導教授 ： 黃鐘揚

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

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

摘要

高階設計資訊被廣泛的應用在現今超大型積體電路的設計上，如：有限狀態機、計數器等等。我們可利用這些高階資訊去輔助設計空間的延展，進一步改善驗證的效率及品質。然而，幾個已存在著眼於高階資訊箤取的相關研究中，都僅能在限定的描述格式下箤取出非常有限的控制結構，如：明確型有限狀態機。在這篇論文中，我們提出一個新穎的技術，能夠精確地箤取出所有的結構，如：明確型有限狀態機、隱含型有限狀態機及計數器。我們於論文中證明幾個演算法中的定理，表示出我們提出的演算法是非常有用的，且不會因為描述方式不同而限制其能力，更不會被侷限在可合成的語法的框架下。在實驗時，我們實際測試幾個真正的設計去呈現出我們的程式在常見的商業化軟體中，依然處於優先的角色。

關鍵字

有限狀態機 ； 暫存器轉移層 ； 設計資訊箤取

並列摘要

High-level design intents such as finite state machine (FSM) and counter are commonly used in modern VLSI design. We can use them to guide the exploration of the design space and thus improve the verification efficiency. However, previous works on high-level intent extraction can only identify very limited constructs such as explicit FSM in restricted coding style. In this work, we propose a novel technique which can extract all the explicit, implicit FSMs and the counter. We also prove with several theorems that our algorithms are very robust and not limited to the coding styles and the HDL synthesizable subset. The experimental results on several real designs demonstrate that our program is superior over existing commercial tools.

並列關鍵字

FSM RTL ； Design Intent ； Extraction

參考文獻

[1] T-H Wang and T. Edsall, “Practical FSM Analysis for Verilog”, Verilog HDL Conference and VHDL International Users Forum, March 1998 Page(s):52 – 58

[9] C-Y Huang and K-Ting Cheng “Using word-level ATPG and modular arithmetic constraint-solving techniques for assertion property checking”, IEEE Trans. on CAD, 20(3): 381-391, 2001

[11] R-C Ho and M. A Horowitz , “Validation Coverage Analysis for Complex Digital Designs”, International Conference on Computer Aided Design 1996, Pages: 146 – 151.

[12] X. Xu, S. Kimura, K. Horikawa, T. Tsuchiya, “Transition-based coverage estimation for symbolic model checking”, ASPDAC.2006 on 24-27 Jan. 2006.

[13] W. Noth and R. Kolla, “Spanning Tree Based State Encoding for Low Power Dissipation”, In Proc of Date, pp 168-174, March 1999.