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