Wenchao Li and Sanjit A. Seshia

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2011-163

December 25, 2011

http://www2.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},
    Year= {2011},
    Month= {Dec},
    Url= {http://www2.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://www2.eecs.berkeley.edu/Pubs/TechRpts/2011/EECS-2011-163.html
%F Li:EECS-2011-163