Sciweavers

Share
DAC
2010
ACM

Scalable specification mining for verification and diagnosis

8 years 7 months ago
Scalable specification mining for verification and diagnosis
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 us...
Wenchao Li, Alessandro Forin, Sanjit A. Seshia
Added 02 Sep 2010
Updated 02 Sep 2010
Type Conference
Year 2010
Where DAC
Authors Wenchao Li, Alessandro Forin, Sanjit A. Seshia
Comments (0)
books