Formal Verification of Pipelined Microprocessors

Dissertation

Abstract

Subject of this thesis is the formal verification of pipelined microprocessors. This includes processors with state of the art schedulers, such as the Tomasulo scheduler and speculation. In contrast to most of the literature, we verify synthesizable design at gate level. Furthermore, we prove both data consistency and liveness. We verify the proofs using the theorem proving system PVS. We verify both in-order and out-of-order machines. For verifying in-order machines, we extend the stall engine concept presented in [MP00]. We describe and implement an algorithm that does the transformation into a pipelined machine. We describe a generic machine that supports speculating on arbitraty values. We formally verify proofs for the Tomasulo scheduling algorithm with reorder buffer.

Excerpts from the Thesis

Chapter 1: Introduction

Downloads

Full text as PDF: diss-kroe.pdf (de) diss-kroe.pdf (us mirror)
Full text as Postscript: diss-kroe.ps.gz (de) diss-kroe.ps.gz (us mirror)
List of known errors

Author

Daniel Kroening
kroening@handshake.de

Current Address:

Daniel Kroening
WEH 3408, CSD
Cargnegie Mellon University
5000 Forbes Av.
Pittsburg, PA 15213
USA

Advisors and Thesis Committee (Gutachter)

Prof. Kurt Mehlhorn, Max-Planck-Institut für Informatik
Priv. Doz. Silvia M. Mueller, IBM Reseach
Prof. Wolfgang J. Paul, Saarland University

Misc

There is a summary of the thesis in the book Ausgezeichnete Informatikdissertationen 2001, published by the Gesellschaft für Informatik, on pages 71-80.