Formal verification of pipelined microprocessors [Elektronische Ressource] / Daniel Kröning

Formal Verification ofPipelined MicroprocessorsDissertationzur Erlangung des Grades Doktor derIngenieurswissenschaften (Dr. Ing.) der¨Naturwissenschaftlich Technischen Fakultat I der¨Universitat des SaarlandesDaniel Kroni¨ ngSaarbruc¨ ken, 2001AbstractSubject of this thesis is the formal verification of pipelined micropro cessors. This includes processors with state of the art schedulers, such asthe Tomasulo scheduler and speculation. In contrast to most of the litera ture, we verify synthesizable design at gate level. Furthermore, we proveboth data consistency and liveness. We verify the proofs using the theoremproving system PVS. We verify both in order and out of order machines.For verifying in order machines, we extend the stall engine concept pre sented in [MP00]. We describe and implement an algorithm that does thetransformation into a pipelined machine. We describe a generic machinethat supports speculating on arbitraty values. We formally verify proofsfor the Tomasulo scheduling algorithm with reorder buffer.KurzzusammenfassungGegenstand dieser Dissertation ist die formale Verifikation von Mikro prozessoren mit Pipeline. Dies beinhaltet auch Prozessoren mit aktuellenScheduling Verfahren wie den Tomasulo Scheduler und spekulativer Aus f¨uhrung. Im Gegensatz zu weiten Teilen der bestehenden Literatur fuhren¨wir die Verifikation auf Gatter-Ebene durch.