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.

Verisoft ist ein nationales Verbundprojekt, das vom bmb+f gefördert wird. Projektpartner aus der Industrie und der akademischen Welt arbeiten in diesem Projekt gemeinsam daran, integrierte Computersysteme durchgehend formal zu verifizieren. Weitere Informationen befinden sich unter http://www.verisoft.de.

Die SB-PRAM ist ein MIMD Parallelrechner mit einem shared main memory und uniformer Speicherzugriffszeit (CRCW-PRAM-Modell). Die Prozessoren sind durch ein Butterfly Netzwerk mit den Speichermodulen verbunden. Jedes SB-PRAM Prozessormodul besteht aus einem selbst konzipierten Prozessor, der über einen erweiterten Berkely-RISC Befehlssatz verfügt, einem lokalen Programmspeicher und einem SCSI-Interface. Die Netzwerkknoten und Speichermodule unterstützen hardwaremäßig konkurrierende Lese- und Schreibzugriffe sowie parallele Präfixoperationen. Die Netzwerkverzögerung wird durch das Pipelining mehrer virtueller Prozessoren (Hardware Threads mit overheadfreiem Umschalten) verborgen. Die Anzahl der Netzwerkstaus wird durch gehashte Adressen reduziert.

Das FiberLink-Projekt wird in Zusammenarbeit mit dem Institut für Technische Physik der Deutschen Luft- und Raumfahrtgesellschaft durchgeführt. Mit steigenden Frequenzen innerhalb von Chips wird die Datenübertragung zwischen einzelnen Chips mehr und mehr zum Bottleneck. Eine wesentliche Steigerung des Durchsatzes ist bei elektrischer Übertragung in Zukunft nicht zu erwarten. Eine optischen Übertragung bringt momentan zwar noch keine Vorteile, verspricht aber mehr Entwicklungspotential. In diesem Projekt wird exemplarisch die Anbindung des Hauptspeichers an den Prozessor-Cache über einen optischen Bus realisiert, um die Vorteile und Machbarkeit dieser Methode zu zeigen.

Im Auftrag des Ministeriums für Bildung, Kultur und Wissenschaft des Saarlandes wird Multimediasoftware entwickelt, die zur Unterstützung des Unterrichts in den saarländischen Schulen eingesetzt werden soll. Die Software besteht jeweils aus einem multimedialen Lehrbuch, das die Lerninhalte anschaulich vermitteln soll, und zusätzlichen Übungsprogrammen, in denen die Schüler das Wissen in Experimenten, Spielen und Übungen anwenden können. Die Software ist genau auf den Lehrplan der Schulen abgestimmt und umfasst die folgenden Themen:

• Mathematik I: Einführung in die Differenzialrechnung
• Mathematik II: Einführung in die Integralrechnung
• Geographie: Plattentektonik
• Musik I: Melodielehre
• Musik II: Harmonie und Rhythmen
• Bildende Kunst: Kompositionslehre

Das Computer Architechture Projekt hat sich zum Ziel gesetzt, einen modernen Prozessor komplett auf Gatterebene zu entwickeln. Dies ermöglicht die Berechnung von Kosten und Zykluszeit und somit eine genaue Analyse der Qualität verschiedener Verfahren wie (Super-)pipelining, Out-of-Order Ausführung oder Caching. Um das Vertrauen in die Korrektheit nicht auf Simuationen stützen zu müssen, wurden über große Teile des Prozessors mathematische Korrektheitsbeweise geführt. Diese bilden die Grundlage für das VAMP-Projekt.

Ziel dieses Projekts ist es, große Teile des interaktiven VAMP-Beweises zu automatisieren. Deshalb integrieren wir automatische Tools in Isabelle/HOL und benutzen diese, um so viele Lemmas und Teilaussagen wie möglich zu lösen.

Ziel des Projektes war die formale Code-Level Verifikation eines Compilers für die C-ähnliche Sprache C0. Der Korrektheitsbeweis besteht aus zwei Teilen:

1. Formale Spezifikation der Code-Generierung im Theorembeweiser Isabelle/HOL.
   Für den funktionalen Code-Generator haben wir beweisen, dass die Ausführung des generierten Assemblercodes für ein bestimmtes C0 Programm auf der abstrakten Assemblermaschine des VAMP-Prozessors eine Simulation der Ausführung des ursprünglichen C0-Programms auf einer abstrakten C0-Maschine darstellt.
2. Im zweiten Teil implementieren wir den C0-Compiler in C0 und zeigen, dass die Compiler-Implementierung in C0 und die Compiler-Spezifikation in Isabelle/HOL den gleichen Assemblercode erzeugen.

In diesem Projekt möchten wir einen Betriebssystemkern spezifizieren und formal verifizieren. Der Betriebssystemkern unterstützt Memory Management ohne Shared Memory, I/O mit Geräten, Prozess-Management und synchrone Interprocess-Communication.

Das Ziel dieses Projektes is Design, Implementierung und formale Verifikation eines einfachen Betriebssystems (SOS). Das SOS ist ein privilegiertes Benutzerprogramm, das die Primitiven des VAMOS Mikrokerns nutzt, um anderen Benutzerprogrammen (den Applikationen) ein vollständiges Betriebssystem anzubieten.

In diesem Projekt formalisieren wir den FlexRay-Standard und designen einen FlexRay-Controller zum Einsatz in einem Automtive-System. FlexRay bietet zahlereiche Mechanismen zur Fehler-Korrektur und Clock-Synchornisation; außerdem garantiert es worst-case Kommunikationszeiten durch statisches Scheduling.

In diesem Projekt untersuchen wir, welche maximale Pipelinetiefe ein Prozessor haben kann. Dazu gehört das Design und die Korrektheit von speziellen stall- und forarding-Schaltkreisen sowie gepipelinete RAM-Zugriffe. Zusätzlich untersuchen wir, welche Pipeline-Tiefe optimal in Bezug auf Benchmarks ist.