Hauptseite |
| Projektübersicht |
| Ziel des VAMP-Projektes ist die formale Verifikation des VAMP-Mikroprozessors. Der VAMP-Prozessor ist eine Variante des 32-Bit DLX Prozessors. Der VAMP besitzt einen Tomasulo-Scheduler für Out-Of-Order Befehlsausführung, geschachtelte präzise Interrupts, eine fünfstufige Pipeline, eine vollständig IEEE konforme Fließkommaeinheit und integrierte Daten- und Instruktionscaches. Die Fließkommaeinheit besteht aus drei Teilen: Addition/Subtraktion, Multiplikation/Division sowie Vergleiche und Typ-Konvertierungen. Es werden Fließkommzahlen einfacher und doppelter Genauigkeit unterstützt. Denormalisierte Zahlen und Fließkomma-Exceptions werden in Hardware behandelt. Die Beweise werden auf dem Gatelevel mit dem Beweissystem PVS von SRI durchgeführt. Die PVS Hardwarespezifikation wird anschließend mit einem Programm (PVS2HDL) automatisch in die Hardwarebeschreibungssprache Verilog übersetzt. Der verifizierte VAMP-Prozessor wird dann auf einem Xilinx-FPGA implementiert. |
| Projektstatus |
| Die formale Verifikation des VAMP-Prozessor mit FPU, Caches, und Tomasulo-Kern ist in PVS 2.3 (patch level 1.2.2.36) abgeschlossen. Das Übersetzungstool PVS2HDL ist fertiggestellt. Der VAMP-Prozessor wurde erfolgreich auf einem Xilinx-FPGA implementiert und getestet. In den schon verifizierten Teilen war dazu keinerlei Hardware-Debugging notwendig.
2005 wurde der VAMP für virtuellen Speicher mit Adreßübersetzung erweitert. Auch hier ist die formale Verifikation im Theorembeweiser PVS abgeschlossen. Die Gruppe von Prof. Peter-Michael Seidel von der SMU in Dallas hat in Zusammenarbeit mit unserem Lehrstuhl den VAMPExplorer entwickelt, ein Tool, das einen intuitiven Zugang zu den umfangreichen VAMP-Sourcen erlaubt. Der VAMPExplorer ist online verfügbar, damit die VAMP-Sourcen den Entwicklern automatischer Methoden leicht als Benchmark für ihre Tools dienen können. |
| Projektmitarbeiter |
|
Dr. Sven Beyer Dr.-Ing. Jakov Dalinger Dr. Christian Jacobi Dr. Dirk Leinenbach Prof. Dr. Wolfgang J. Paul |
