Title :
A Technique for Test Coverage Closure Using GoldMine
Author :
Liu, Lingyi ; Sheridan, David ; Tuohy, William ; Vasudevan, Shobha
Author_Institution :
Dept. of Electr. & Comput. Eng., Univ. of Illinois at Urbana-Champaign, Urbana, IL, USA
fDate :
5/1/2012 12:00:00 AM
Abstract :
We propose a methodology to generate input stimulus to achieve coverage closure using GoldMine, an automatic assertion generation engine that uses data mining and formal verification. GoldMine mines the simulation traces of a behavioral register transfer level (RTL) design using a decision tree based learning algorithm to produce candidate assertions. These candidate assertions are passed to a formal verification engine. If a candidate assertion is false, a counterexample trace is generated. In this paper, we feed these counterexample traces to iteratively refine the original simulation trace data. We introduce an incremental decision tree to mine the new traces in each iteration. The algorithm converges when all the candidate assertions are true. We formally prove that our algorithm will always converge and capture the complete functionality of each output of a sequential design on convergence. We show that our method always results in a monotonic increase in simulation coverage. We also present an output-centric notion of coverage, and argue that we can attain coverage closure with respect to this notion of coverage. We elaborate the technique step by step using a nontrivial arbiter design. Experimental results to validate our arguments are presented on several designs from Rigel, OpenRisc, and SpaceWire. Some practical limitations to achieve 100% coverage and the differences between final decision tree and binary decision diagram are discussed.
Keywords :
binary decision diagrams; data mining; decision trees; formal verification; hardware description languages; iterative methods; learning (artificial intelligence); GoldMine; OpenRisc; Rigel; SpaceWire; automatic assertion generation engine; behavioral register transfer level design; binary decision diagram; data mining; decision tree based learning algorithm; formal verification engine; input stimulus generation; iterative refinement; nontrivial arbiter design; sequential design; simulation trace mining; test coverage closure; Algorithm design and analysis; Convergence; Data mining; Data models; Decision trees; Numerical models; Registers; Assertion; data mining; design validation; static analysis;
Journal_Title :
Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
DOI :
10.1109/TCAD.2011.2177461