Electrical Engineering
      and Computer Sciences

Electrical Engineering and Computer Sciences

COLLEGE OF ENGINEERING

UC Berkeley

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