GoldMine: Automatic Assertion Generation and Achieving Test Coverage Closure

Speaker Prof. Shobha Vasudevan
ECE, University of Illinois at Urbana-Champaign
Urbana, Illinois
CECS Host Nikil Dutt
Location Donald Bren Hall (DBH) 4011
Date & Time June 2, 2011
Refreshments at 1:30 pm, Lecture begins at 2:00pm
Abstract Assertions are ubiquitous in the modern system design cycle. They are used in pre-Silicon verification, post-Silicon validation and debug, emulation, reliability checking, and many related functional assurance phases. Assertion generation is an intensely manual, time-intensive task. GoldMine, developed by my group in UIUC, is an assertion generation software that uses a combination of data mining and static analysis of the design. GoldMine uses formal verification to guide the data mining algorithms. GoldMine assertions are attested by designers, as adding value to the verification process. In the first part of my talk, I will present the function and working of this engine, as well as its recent application at the specification level. 

Counterexample feedback from formal verification of an assertion can be used to grow the size of the data set that is mined by GoldMine. When iteratively applied, this data set eventually captures the entire behavior. This data set now forms a test suite where coverage closure can be achieved. This algorithm for monotonically increasing coverage of validation inputs is presented in the second part of my talk. I will also discuss how GoldMine can be applied in the context of soft error detection and emulation.

Biography

Shobha Vasudevan is an assistant professor of Computer Engineering in the ECE Department, at the Univ of Illinois. She obtained her PhD and MS degrees from the University of Texas at Austin. Her research interests are in design verification, validation, reliability, software testing, data mining and formal verification. She is a recepient of the 2010 NSF CAREER award and the YWCA leadership in Science award.