SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

Inverting the Abstraction Mapping: A Methodology for Hardware Verification
 by David Cryluk.


Abstract. Abstraction mappings have become a standard approach to verifying the correctness of processors. When used in a straightforward manner this approach suffers from generating extremely large intermediate terms that have to be simplified.

In an interactive theorem prover the complete expansion of the abstraction mapping is not even possible. Yet, with human guidance it is interactive theorem proving that is applied to examples too large to be handled by automated methods.

We present a methodology for verifying the correctness of processors that aims to limit the size of intermediate terms generated in an interactive proof and to manage the complexity of the proof search.

The main idea of this methodology is that, instead of expanding the abstraction mapping and thereby introduce large implementation terms into the specification, we try to identify sub-terms of implementation terms that can be replaced by specification state variables. This is done by inverting the equations defining the abstraction mapping so to rewrite implementation terms into abstract state variables.

This method has been successfully applied to the verification of the DLX processor. It has also been applied to the verification of the ALU pipeline and Saxe pipeline and has simplified their proofs.

Finally, lessons learned from this methodology can help develop better heuristics employed by automatic methods.



About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2019 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy