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

Sujets

• Informatik

Informations

• Publié par: universitat_des_saarlandes
• Publié le: 01 janvier 2004
• Nombre de lectures: 16
• Langue: Deutsch
• Poids de l'ouvrage: 1 Mo

Extrait

Formal Verification of
Pipelined Microprocessors
Dissertation
zur Erlangung des Grades Doktor der
Ingenieurswissenschaften (Dr. Ing.) der
¨Naturwissenschaftlich Technischen Fakultat I der
¨Universitat des Saarlandes
Daniel Kroni¨ ng
Saarbruc¨ ken, 2001Abstract
Subject of this thesis is the formal verification of pipelined micropro
cessors. This includes processors with state of the art schedulers, such as
the Tomasulo scheduler and speculation. In contrast to most of the litera
ture, 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 pre
sented 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.
Kurzzusammenfassung
Gegenstand dieser Dissertation ist die formale Verifikation von Mikro
prozessoren mit Pipeline. Dies beinhaltet auch Prozessoren mit aktuellen
Scheduling 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. Des weitern beweisen wir
sowohl Datenkonsistenz als auch eine obere Schranke fur¨ die Ausfuh ¨
rungszeit. Die Beweise werden mit dem Theorem Beweissystem PVS
verifiziert. Es werden sowohl in order Maschinen als auch out of order
Maschinen verifiziert. Zur Verifikation der in order Maschinen erweitern
wir die Stall Engine aus [MP00]. Wir beschreiben und Implementieren ein
Verfahren das die Transformation in die “pipelined machine” durchfuhrt.¨
Wir beschreiben eine generische Maschine die Spekulation auf beliebige
Werte erlaubt. Wir verifizieren die Beweise fur¨ den Tomasulo Scheduler
mit Reorder Buffer.Extended Abstract
Microprocessors are in use in many safety critical environments, such as
cars or planes. We therefore consider the correctness of such components
as a matter of vital importance. Testing microprocessors is limited by the
huge state space of modern microprocessors. We therefore think formal
verification is the sole way to obtain a guarantee.
This formal verification should be done such that any third party is able
to verify the correctness with low effort, i.e., we aim to provide a proof
of correctness that can be checked mechanically. In particular, we think
that all critical designs should be delivered in form of a four tuple: 1)
the design itself, 2) a specification, 3) a human readable proof, and 4) a
machine verified proof.
In this thesis, we present proofs of correctness for complex micropro
cessors. Designing microprocessors is considered an error-prone process.
A well known example for this is the Pentium FDIV bug [Coe95, Pra95].
In this thesis, we provide a rigorously formal approach to hardware veri
fication. The designs presented in this thesis include state of the art sched
ulers, such as the Tomasulo scheduler [Tom67] and speculation. In con
trast to most of the literature, the designs we provide are very close to
gate level. In particular, we are synthesizing some of the designs for the
XILINX FPGA series.
These designs are of high complexity, and so are the proofs. In contrast
to [MP95, Lei99, MP00], the proofs are machine verified using the theorem
proving system PVS [CRSS94]. We do not present the original PVS proof
in this thesis but aim to provide comprehensible paper-and pencil proofs.
In order to verify sequential machines, we extend the data consistency
invariant given in [MP00] by defining a “correct value” of an implementa
tion register such as IR 2. Given the correctness of functional components
such as the ALU, this allows for an almost fully automated proof of the
data consistency of the prepared sequential machine using PVS. We ar-
gue that the correct functional components provide correct results if given
correct inputs.
We extend the stall engine concept presented in [MP00] by providing
:a fully generic stall engine design. In contrast to [MP00], our stall en
gine design supports an arbitrary number of stages and allows for stalling
(and therefore clocking) all stages independently. Furthermore, it supports
pipeline bubble removal, i.e., the stages are clocked whenether the in order
property permits this. This includes that bubbles are removed from the
pipeline if necessary. We formally verify data consistency and liveness
properties for this stall engine.
Using this extended stall engine, we improve the process of transforming
the prepared sequential machine into the pipelined machine by providing
a tool that does this transformation automatically. This includes the gener-
ation for forwarding and interlock hardware.
We then prove the data consistency of the pipelined machine. We do
so by showing that the inputs of the pipeline stages are correct. Using this
fact, we argue the correctness of the output values as we do for the prepared
sequential machine, since the functional components of the machines are
identical.
We present a generic approach to speculative execution and propose a
data consistency criterion for such a machine. We then apply this method
in order to implement and prove DLX pipelines with branch prediction
and precise interrupts. It is a well known fact that both techniques are im-
plemented using speculation [SP88]. However, to the best of our knowl-
edge, implementing both techniques as an instance of a generic speculation
mechanism is done for the first time.
Besides the in order pipelines, we verify the correctness of the Tomasulo
scheduling algorithm with reorder buffer as described in [KMP99]. The re
order buffer realizes in order termination, which allows implementing pre
cise interrupts. The proof of correctness covers the arguments neccessary
to show the uniqueness of the tags.
Furthermore, we rigorously prove the liveness of all machines we de
sign, i.e., we prove that any given instruction sequence is executed within
a finite amount of time. Although critical, liveness issues are often not
covered in the open literature.Zusammenfassung
Mikroprozessoren werden in vielen sicherheitskritischen Bereichen ein
gesetzt, wie beispielsweise in Automobilen oder Flugzeugen. Wir erachten
daher die Korrektheit solcher Komponenten als lebenswichtig. Der Test
von Prozessoren ist durch den extrem großen Zustandsraum moderner Pro
zessoren nur eingeschrankt¨ moglich.¨ Wir sind daher der Meinung, daß
formale Verifikation die einzige Moglichk¨ eit darstellt, eine Garantie zu er-
halten.
Diese formale Verifikation sollte so durchgefuhrt¨ werden, daß Dritten
die Moglichk¨ eit offen steht, die Korrektheit mit geringen Aufwand nachzu
vollziehen. Wir wollen daher einen Beweis zur Verfugung¨ stellen, der au
tomatisiert uberpr¨ uft¨ werden kann. Insbesondere sollten alle kritischen De-
signs in Form von vier-Tupeln ausgeliefert werden: 1) das Design selbst,
2) eine Spezifikation, 3) ein manuell nachvollziehbarer Beweis, und 4) ein
maschinell verifizierbarer Beweis.
Gegenstand dieser Dissertation sind Korrektheitsbeweise fu¨r komplexe
Mikroprozessoren. Die Erstellung von Mirkoprozessordesigns gilt als feh
leranfallig.¨ Ein bekanntes Beispiel ist der Pentium FDIV bug [Coe95,
Pra95].
In dieser Dissertation wird das Problem der Korrektheit von Hardware
streng formal behandelt. Die Designs beinhalten Prozessoren mit aktuellen
Scheduling Verfahren, wie beispielsweise dem Tomasulo Scheduler aus
[Tom67] und spekulativer Ausfuhrung.¨ Im Gegensatz zu weiten Teilen
der bestehenden Literatur sind die Designs auf Gatter-Ebene spezifiziert.
Insbesondere werden einige der Designs fur¨ die XILINX FPGA Serie syn
thetisiert.
Die Designs haben hohe Komplexitat,¨ was sich auf die Beweise aus
wirkt. Im Gegensatz zu [MP95, Lei99, MP00] sind die Beweise mit dem
Theorem Beweissystem PVS verifiziert. Wir geben in dieser Dissertation
nicht den originalen PVS Beweis an, sondern versuchen einen nachvol
lziehbaren Beweis in ublicher¨ mathematischer Notation anzugeben.
Um sequentielle Maschinen zu verifizieren, erweitern wir die Datenkon
sistenz Invariante aus [MP00] indem wir einen “korrekten Wert” eines Im-
plenentation Registers wie beispielsweise IR 2 definieren. Gegeben die
:Korrektheit der funktionalen Komponenten, wie beispielsweise der ALU,
erlaubt uns dies den Beweis der Datenkonsistenz der prapariert¨ sequen
tiellen Maschine in PVS fast vollig¨ zu automatisieren. Wir argumentieren,
daß die funktionellen Komponenten korrekte Ergebnisse liefern wenn sie
korrekte Eingaben erhalten.
Wir erweitern das Konzept der “stall engine” aus [MP00] indem wir eine
vollstandig¨ generische stall engine angeben. Im Gegensatz zu der stall en
gine aus [MP00], erlaubt unsere stall engine eine beliebige Anzahl von
Stufen und ermoglicht¨ es, alle Stufen unabhangig¨ voneinander anzuhalten.
Des weiteren unterstutzt¨ unsere stall engine das Entfernen von “pipeline
bubbles