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.
R&D Divisions