Specification Mining for Digital Circuits with Applications on Verification and Diagnosis

Software and hardware systems are often built without detailed documentation. The correctness of these systems can only be verified as well as the specifications are written. The lack of sufficient specifications often leads to misses of critical bugs, design re-spins, and time-to-market slips. In this paper, we address this problem by mining specification dynamically from simulation traces. 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 error-labeled traces are used to automatically pinpoint the sources of error. In this work, we focus on traces from digital circuits, but any ordered trace of events is amenable to this analysis. We demonstrate the effectiveness of our approach on industrial-size examples.