Towards coverage closure

Using GoldMine assertions for generating design validation stimulus

Lingyi Liu, David Sheridan, William Tuohy, Shobha Vasudevan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationProceedings - Design, Automation and Test in Europe Conference and Exhibition, DATE 2011
Pages173-178
Number of pages6
StatePublished - May 31 2011
Event14th Design, Automation and Test in Europe Conference and Exhibition, DATE 2011 - Grenoble, France
Duration: Mar 14 2011Mar 18 2011

Publication series

NameProceedings -Design, Automation and Test in Europe, DATE
ISSN (Print)1530-1591

Other

Other14th Design, Automation and Test in Europe Conference and Exhibition, DATE 2011
CountryFrance
CityGrenoble
Period3/14/113/18/11

Fingerprint

Decision trees
Engines
Learning algorithms
Data mining
Formal verification

ASJC Scopus subject areas

  • Engineering(all)

Cite this

Liu, L., Sheridan, D., Tuohy, W., & Vasudevan, S. (2011). Towards coverage closure: Using GoldMine assertions for generating design validation stimulus. In Proceedings - Design, Automation and Test in Europe Conference and Exhibition, DATE 2011 (pp. 173-178). [5763038] (Proceedings -Design, Automation and Test in Europe, DATE).

Towards coverage closure : Using GoldMine assertions for generating design validation stimulus. / Liu, Lingyi; Sheridan, David; Tuohy, William; Vasudevan, Shobha.

Proceedings - Design, Automation and Test in Europe Conference and Exhibition, DATE 2011. 2011. p. 173-178 5763038 (Proceedings -Design, Automation and Test in Europe, DATE).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Liu, L, Sheridan, D, Tuohy, W & Vasudevan, S 2011, Towards coverage closure: Using GoldMine assertions for generating design validation stimulus. in Proceedings - Design, Automation and Test in Europe Conference and Exhibition, DATE 2011., 5763038, Proceedings -Design, Automation and Test in Europe, DATE, pp. 173-178, 14th Design, Automation and Test in Europe Conference and Exhibition, DATE 2011, Grenoble, France, 3/14/11.
Liu L, Sheridan D, Tuohy W, Vasudevan S. Towards coverage closure: Using GoldMine assertions for generating design validation stimulus. In Proceedings - Design, Automation and Test in Europe Conference and Exhibition, DATE 2011. 2011. p. 173-178. 5763038. (Proceedings -Design, Automation and Test in Europe, DATE).
Liu, Lingyi ; Sheridan, David ; Tuohy, William ; Vasudevan, Shobha. / Towards coverage closure : Using GoldMine assertions for generating design validation stimulus. Proceedings - Design, Automation and Test in Europe Conference and Exhibition, DATE 2011. 2011. pp. 173-178 (Proceedings -Design, Automation and Test in Europe, DATE).
@inproceedings{6e5bf63cf9f74120a251c4ee47e4777a,
title = "Towards coverage closure: Using GoldMine assertions for generating design validation stimulus",
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.",
author = "Lingyi Liu and David Sheridan and William Tuohy and Shobha Vasudevan",
year = "2011",
month = "5",
day = "31",
language = "English (US)",
isbn = "9783981080179",
series = "Proceedings -Design, Automation and Test in Europe, DATE",
pages = "173--178",
booktitle = "Proceedings - Design, Automation and Test in Europe Conference and Exhibition, DATE 2011",

}

TY - GEN

T1 - Towards coverage closure

T2 - Using GoldMine assertions for generating design validation stimulus

AU - Liu, Lingyi

AU - Sheridan, David

AU - Tuohy, William

AU - Vasudevan, Shobha

PY - 2011/5/31

Y1 - 2011/5/31

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=79957542440&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=79957542440&partnerID=8YFLogxK

M3 - Conference contribution

SN - 9783981080179

T3 - Proceedings -Design, Automation and Test in Europe, DATE

SP - 173

EP - 178

BT - Proceedings - Design, Automation and Test in Europe Conference and Exhibition, DATE 2011

ER -