# A Sparse Coding Method for Specification Mining and Error Localization

### Wenchao Li and Sanjit A. Seshia

###
EECS Department

University of California, Berkeley

Technical Report No. UCB/EECS-2011-163

December 25, 2011

### http://www.eecs.berkeley.edu/Pubs/TechRpts/2011/EECS-2011-163.pdf

Formal specifications play a central role in the design, verification, and debugging of systems. We consider the problem of mining specifications from simulation or execution traces of reactive systems with a special focus on digital circuits. We propose a novel sparse coding method that can extract specifications in the form of a set of basis subtraces. For a set of finite subtraces each of length p, we introduce the sparse Boolean basis problem as the decomposition of each subtrace into a Boolean combination of only a small number of basis subtraces of the same dimension. The contributions of this paper are (1) we formally define the sparse Boolean basis problem and propose a graph-based algorithm to solve it; (2) we demonstrate that we can mine useful specifications using our sparse coding method; (3) we show that the computed bases can be used to do simultaneous error localization and error explanation in a setting that is especially applicable to post-silicon debugging.

BibTeX citation:

@techreport{Li:EECS-2011-163, Author = {Li, Wenchao and Seshia, Sanjit A.}, Title = {A Sparse Coding Method for Specification Mining and Error Localization}, Institution = {EECS Department, University of California, Berkeley}, Year = {2011}, Month = {Dec}, URL = {http://www.eecs.berkeley.edu/Pubs/TechRpts/2011/EECS-2011-163.html}, Number = {UCB/EECS-2011-163}, Abstract = {Formal specifications play a central role in the design, verification, and debugging of systems. We consider the problem of mining specifications from simulation or execution traces of reactive systems with a special focus on digital circuits. We propose a novel sparse coding method that can extract specifications in the form of a set of basis subtraces. For a set of finite subtraces each of length p, we introduce the sparse Boolean basis problem as the decomposition of each subtrace into a Boolean combination of only a small number of basis subtraces of the same dimension. The contributions of this paper are (1) we formally define the sparse Boolean basis problem and propose a graph-based algorithm to solve it; (2) we demonstrate that we can mine useful specifications using our sparse coding method; (3) we show that the computed bases can be used to do simultaneous error localization and error explanation in a setting that is especially applicable to post-silicon debugging.} }

EndNote citation:

%0 Report %A Li, Wenchao %A Seshia, Sanjit A. %T A Sparse Coding Method for Specification Mining and Error Localization %I EECS Department, University of California, Berkeley %D 2011 %8 December 25 %@ UCB/EECS-2011-163 %U http://www.eecs.berkeley.edu/Pubs/TechRpts/2011/EECS-2011-163.html %F Li:EECS-2011-163