Projektinhalt und -ziele

Im Projekt VerSys geht es um die Entwicklung und Erforschung neuer Methoden der Computeralgebra, um die Korrektheit von Chip-Entwürfen nachzuweisen. Die zentrale Frage ist also, ob ein Chip tatsächlich die mathematischen Funktionen korrekt bereitstellt, die bei dessen Entwurf intendiert waren.

Heutige Systems-on-Chip (SoCs) sind aus einer Vielzahl von oft hoch komplexen, nebenläufig arbeitenden Komponenten zusammengesetzt, die miteinander über leistungsfähige Kommunikationsstrukturen vernetzt sind. Zudem erfüllen verschiedene Blöcke auf einem Chip aus Effizienzgründen oft mehrere Aufgaben; je nachdem, welche logische Verschaltung auf dem Chip zur Laufzeit gerade aktiviert ist. Tatsächlich stellt die Verifikationsaufgabe bei Chips heute mit 60 bis 80 Prozent der Entwicklungskosten den größten Anteil an den Herstellungskosten überhaupt dar. Chips gelangen deshalb zum Teil erst verhältnismäßig spät nach der Designphase in die Massenproduktion. Und Fehler sind auf jeden Fall zu vermeiden, da sie neben unbrauchbaren Chips und den damit verbundenen Produktionskosten einen für den Hersteller schweren Imageschaden bedeuten können. Ein Beispiel dafür ist der so genannte Pentium-Bug, der auf eine fehlerhafte Division in einem arithmetischen Block zurückging, siehe www.nytimes.com

Als Konsequenz aus der weiter steigenden Komplexität setzen die Chip-Hersteller auf die konsequente Automatisierung der Verifikationsaufgabe, soweit dies möglich ist. Dabei spielen traditionell logische Verifizierungswerkzeuge eine große Rolle. Doch schon für Funktionen von verhältnismäßig kleiner mathematischer Komplexität, z.B. 32-Bit-Multiplizierer, ist die Anwendung logischer Verifizierer nicht mehr praktikabel: Es können keine lückenlosen Korrektheitsbeweise mehr automatisch geführt werden.

Auch die Simulation einer möglichst großen Menge von Eingabewerten, für die das durch den Chip berechnete Ergebnis mit dem mathematisch korrekten Wert übereinstimmen muss, vermag die Richtigkeit des Chip-Designs nur zu einer gewissen Wahrscheinlichkeit sicherzustellen.

Der neue, im Projekt VerSys verfolgte Ansatz modelliert hingegen arithmetische Funktionen des Chips nicht mehr als logische sondern als algebraische Problemstellungen. Damit werden bekannte Ergebnisse und Algorithmen aus der Computeralgebra, wie z.B. die Berechnung von Gröbnerbasen für polynomiale Ideale, mehr oder weniger direkt anwendbar auf das Problem der Chipverifikation. Zudem existieren bereits effiziente Implementierungen, z.B. SINGULAR (www.singular.uni-kl.de) und PolyBoRi (polybori.sourceforge.net), und werden in umfassenden Algebra-Suites zusammengefasst; siehe z.B. SAGE (www.sagemath.org).

Andererseits erfordern neue Applikationen wie die Chipverifikation die Anpassung bekannter Algorithmen. Damit treiben sie die mathematische Forschung auf dem Gebiet der Computeralgebra in anwendungsorientierter Weise voran.

Vorgängerprojekte und erste Ergebnisse in VerSys zeigen, dass mit Computeralgebra und speziell durch die Kombination logischer und computeralgebraischer Ansätze Verifikationsaufgaben gelöst werden können, die zuvor als praktisch unlösbar galten.