以正規方法驗證模擬測試序列品質

由於電路設計日趨複雜化，電路正確性的驗證已是不可或缺的一個步驟。模擬是目前普遍用於驗證邏輯閘階層或暫存器移轉階層電路設計的功能的方法，然而這種方法對於人工輸入或隨機產生的模擬測試序列品質的評估，雖然已有數種涵蓋率的技術來作量化的比較，但是對於驗證完整度的評量，仍然缺乏一種具有足夠鑑別率的量化量度。因此在本論文中，我們以正規驗證技術的循序深度計算與可達性分析，推衍出可供設計者評估模擬測試序列品質與模擬涵蓋率的合理量度，並且亦修正前述量度以因應正規驗證在較大電路的運算資源不足問題。此外，本論文所提出的量度是根據循序深度的模擬正確度、限定模擬時間中布林狀態空間中狀態或cubes的模擬完整度、循序深度的模擬效能以及設計者加權等需求而決定。

關鍵字

模擬；正規驗證；二元決策圖；涵蓋率量度；循序深度；可達性分析

並列摘要

Due to the increasing design complexity, verification of modern VLSI designs has become an essential work in the design flow. Simulation is predominant verification method to verify the functionality of gate level or register-transfer level (RTL) design nowadays. However, it lacks one quantitative metric with enough discrimination to verify the simulation completeness although there exist several coverage metrics for qualifying the test sequence manually defined or randomly generated in simulation. Accordingly, sequential depth computation and reachability analysis of the formal verification techniques are employed to derive or infer the feasible metrics for measuring the quality of test sequence and coverage of simulation. Hence, a modified version of the mentioned metric is proposed to overcome the problem of failure in sequential depth computation and BDD (binary decision diagrams) of transition relationship construction due to the system resource explosion. The proposed metrics consist of the requirements of simulation correctness of sequential depth, simulation completeness of states or cubes of Boolean state space in limited simulation timeframe, simulation performance of sequential depth and weighting in accordance with designer’s preference or concern of the simulation.

並列關鍵字

Simulation ； Formal Verification ； BDD (Binary Decision Diagrams) ； coverage metric ； sequential depth ； reachability analysis

參考文獻

[4] Richard C. Ho and Mark A. Horowitz, “Validation Coverage Analysis for Complex Digital Designs”, Int’l Conf. on Computer Aided Design, Nov. 1996.

[5] Dinos Moundanos, Jacob A. Abraham, and Yatin V. Hoskote, “Abstraction Techniques for Validation Coverage Analysis and Test Generation”, IEEE Trans. on Computer, Vol. 47, no. 1, pp. 2-14, Jan. 1998.

[7] Vishnu C. Vamjamv, “Strategies for SAT-based Formal Verification”, PhD Dissertation, Department of Electrical and Computer Engineering, Virginia Polytechnic Institute and State University, Jan. 2007.

[8] J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill, “Sequential Circuit Verification Using Symbolic Model Checking”, 27th Design Automatic Conf., June 1990.

[9] H. Iwashita, T. Nakata, and F. Hirose, “CTL Model Checking Based on Forward State Traversal”, Int’l Conf. on Computer Aided Design, Nov. 1996.

國際替代計量

以正規方法驗證模擬測試序列品質

全文下載

主題瀏覽