Scalable Specification Mining for Verification and Diagnosis

Wenchao Li, Alessandro Forin, and Sanjit A. Seshia. Scalable Specification Mining for Verification and Diagnosis. In Proceedings of the Design Automation Conference (DAC), pp. 755–760, June 2010.

Download

[pdf] 

Abstract

Effective system verification requires good specifications. The lack of sufficient specifications can lead to misses of critical bugs, design re-spins, and time-to-market slips. In this paper, we present a new technique for mining temporal specifications from simulation or execution traces of a digital hardware design. Given an execution trace, we mine recurring temporal behaviors in the trace that match a set of pattern templates. Subsequently, we synthesize them into complex patterns by merging events in time and chaining the patterns using inference rules. We specifically designed our algorithm to make it highly efficient and meaningful for digital circuits. In addition, we propose a pattern-mining diagnosis framework where specifications mined from correct and erroneous traces are used to automatically localize an error. We demonstrate the effectiveness of our approach on industrial-size examples by mining specifications from traces of over a million cycles in a few minutes and use them to successfully localize errors of different types to within module boundaries.

BibTeX

@inproceedings{li-dac10,
 author = {Wenchao Li and Alessandro Forin and Sanjit A. Seshia},
 title = "Scalable Specification Mining for Verification and Diagnosis",
 booktitle = "Proceedings of the Design Automation Conference (DAC)", 
 pages = "755--760", 
 month = "June", 
 year = "2010",
 abstract = {
Effective system verification requires good specifications. The lack of sufficient specifications can lead to misses of critical bugs, design re-spins, and time-to-market slips. In this paper, we present a new technique for mining temporal specifications from simulation or execution traces of a digital hardware design. Given an execution trace, we mine recurring temporal behaviors in the trace that match a set of pattern templates. Subsequently, we synthesize them into complex patterns by merging events in time and chaining the patterns using inference rules. We specifically designed our algorithm to make it highly efficient and meaningful for digital circuits. In addition, we propose a pattern-mining diagnosis framework where specifications mined from correct and erroneous traces are used to automatically localize an error. We demonstrate the effectiveness of our approach on industrial-size examples by mining specifications from traces of over a million cycles in a few minutes and use them to successfully localize errors of different types to within module boundaries. 
 },
}