Electrical Engineering
      and Computer Sciences

Electrical Engineering and Computer Sciences

COLLEGE OF ENGINEERING

UC Berkeley

Learning Conditional Abstractions

Bryan Brady and Sanjit A. Seshia

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2011-24
April 5, 2011

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

Abstraction is central to formal verification. In term-level abstraction, the design is abstracted using a fragment of first-order logic with background theories, such as the theory of uninterpreted functions with equality. The main challenge in using term-level abstraction is determining what components to abstract and under what conditions. In this paper, we present an automatic technique to conditionally abstract register transfer level (RTL) hardware designs to the term level. Our approach is a layered approach that combines random simulation and machine learning inside a counter-example guided abstraction refinement (CEGAR) loop. First, random simulation is used to determine modules that are candidates for abstraction. Next, machine learning is used on the resulting simulation traces to generate candidate conditions under which those modules can be abstracted. Finally, a verifier is invoked. If spurious counter-examples arise, we refine the abstraction by performing a further iteration of random simulation and machine learning. We present an experimental evaluation on processor and low-power designs.


BibTeX citation:

@techreport{Brady:EECS-2011-24,
    Author = {Brady, Bryan and Seshia, Sanjit A.},
    Title = {Learning Conditional Abstractions},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2011},
    Month = {Apr},
    URL = {http://www.eecs.berkeley.edu/Pubs/TechRpts/2011/EECS-2011-24.html},
    Number = {UCB/EECS-2011-24},
    Abstract = {Abstraction is central to formal verification. In term-level abstraction, the design is abstracted using a fragment of first-order logic with background theories, such as the theory of uninterpreted functions with equality. The main challenge in using term-level abstraction is determining what components to abstract and under what conditions. In this paper, we present an automatic technique to conditionally abstract register transfer level (RTL) hardware designs to the term level. Our approach is a layered approach that combines random simulation and machine learning inside a counter-example guided abstraction refinement (CEGAR) loop. First, random simulation is used to determine modules that are candidates for abstraction. Next, machine learning is used on the resulting simulation traces to generate candidate conditions under which those modules can be abstracted. Finally, a verifier is invoked.  If spurious counter-examples arise, we refine the abstraction by performing a further iteration of random simulation and machine learning. We present an experimental evaluation on processor and low-power designs.}
}

EndNote citation:

%0 Report
%A Brady, Bryan
%A Seshia, Sanjit A.
%T Learning Conditional Abstractions
%I EECS Department, University of California, Berkeley
%D 2011
%8 April 5
%@ UCB/EECS-2011-24
%U http://www.eecs.berkeley.edu/Pubs/TechRpts/2011/EECS-2011-24.html
%F Brady:EECS-2011-24