Title :
Towards coverage closure: Using GoldMine assertions for generating design validation stimulus
Author :
Liu, Lingyi ; Sheridan, David ; Tuohy, William ; Vasudevan, Shobha
Author_Institution :
Dept. of ECE, Univ. of Illinois at Urbana-Champaign, Urbana, IL, USA
Abstract :
We present a methodology to generate input stimulus for design validation 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 work, 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 prove that our algorithm will always converge and capture the complete functionality of an output 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. Experimental results to validate our arguments are presented on several designs from Rigel, OpenRisc and SpaceWire.
Keywords :
data mining; decision trees; formal verification; learning (artificial intelligence); GoldMine assertion; assertion generation engine; behavioral register transfer level design; coverage notion; data mining; decision tree based learning algorithm; design validation stimulus; formal verification; incremental decision tree; Algorithm design and analysis; Buildings; Convergence; Data models; Decision trees; Measurement; Registers;
Conference_Titel :
Design, Automation & Test in Europe Conference & Exhibition (DATE), 2011
Conference_Location :
Grenoble
Print_ISBN :
978-1-61284-208-0
DOI :
10.1109/DATE.2011.5763038