Learning Conditional Abstractions

Bryan Brady, Randal E. Bryant, and Sanjit A. Seshia. Learning Conditional Abstractions. In Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 116–124, October 2011.

Download

[pdf] 

Abstract

Abstraction is central to formal verification. In term-levelabstraction, the design is abstracted using a fragment offirst-order logic with background theories, such as the theory ofuninterpreted functions with equality. The main challenge in usingterm-level abstraction is determining what components to abstractand under what conditions. In this paper, we present an automatictechnique to conditionally abstract register transfer level (RTL)hardware designs to the term level. Our approach is a layeredapproach that combines random simulation and machine learninginside a counter-example guided abstraction refinement (CEGAR)loop. First, random simulation is used to determine modules thatare candidates for abstraction. Next, machine learning is used on theresulting simulation traces to generate candidate conditions underwhich those modules can be abstracted. Finally, a verifier is invoked.If spurious counter-examples arise, we refine the abstraction byperforming a further iteration of random simulation and machinelearning. We present an experimental evaluation on processor andlow-power designs.

BibTeX

@InProceedings{brady-fmcad11,
  author = 	 {Bryan Brady and Randal E. Bryant and Sanjit A. Seshia},
  title = 	 {Learning Conditional Abstractions},
  booktitle = {Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD)},
  month = {October},
  year = 	 {2011},
  pages = "116--124",
  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.},
}