TP3: Korrektes Industrielles Hardware/Software-System — Zuverlässige Chips durch mathematische Beweise

In dem vom Bundesministerium für Bildung und Forschung geförderten Projekt Verisoft rückt der bisher für utopisch gehaltene Korrektheitsnachweis für einen großen industriellen Prozessor in greifbare Nähe.

Üblicherweise werden Schaltungsentwürfe vor der Fertigung durch umfangreiche Simulationen überprüft, um logische Designfehler — d.h. das Gros aller Fehler im Entwurf — rechtzeitig auszuschließen. Da diese Verfahren bei der heutigen Designkomplexität von vielen Millionen Transistoren längst an ihre Grenzen gestoßen sind, arbeiten Forscher in Industrie und Hochschulen an formalen Verifikationstechniken: Dabei werden nicht einzelne Abläufe simuliert, sondern die Übereinstimmung der Logik einer Schaltung mit ihrer Spezifikation im mathematischen Sinne bewiesen.

In das Projekt Verisoft bringt Infineon sein Know-how im Prozessor-Design ebenso ein, wie seine im Jahre 2003 mit dem deutschen EDA-Achievement-Award ausgezeichnete formale Verifikationstechnik CVE (Circuit Verification Environment).

In Zusammenarbeit mit Infineons akademischen Partnern im Projekt Verisoft — der Universität des Saarlandes sowie der Technischen Universität München — wird diese Technik durch die Entwicklung neuer, rechnergestützter Beweisverfahren für die frühen Entwurfsphasen ergänzt.

Im Januar 2005 erreichten Meilenstein wurde anhand des Infineon-Prozessors TriCore 2, dem zukünftigen „Flaggschiff“ der 32 bit-Microcontrollerfamilie von Infineon, erstmals der Nachweis erbracht, dass diese innovative Technik auf hochkomplexe Designs anwendbar ist, und diese auch zukünftig beherrschbar bleiben.

Formale Methoden prädestinieren sich aufgrund der Sicherheit ihrer Aussagen als die entscheidende neue Komponente, um in Ergänzung etablierter Verfahren — wie der Simulation — den Durchbruch beim Entwurf robuster, de facto fehlerfreier Designs zu schaffen und gleichzeitig den iterativen Verifikationsprozess signifikant zu verkürzen.

Für diesen Nachweis wurde der Prozessorkern mit seinen bis zu sechsstufigen Pipelines und nahezu der gesamte reichhaltige Befehlssatz vollständig formal spezifiziert. Bereits 5 Monate vor Abschluss der ersten Phase von Verisoft sind ca. 70% der gesamten Funktionalität des TriCore 2-Kerns verifiziert.

Obwohl die Arbeiten noch nicht abgeschlossen sind, sind die daraus resultierenden Verbesserungen unmittelbar in das Design eingeflossen. So wird Infineon den TriCore 2, der unter anderem im Highend der Automobilelektronik eingesetzt werden soll, auf einem bisher unerreichten Qualitätsniveau anbieten können.

Die geplante Weiterentwicklung des Verfahrens soll dessen Anwendung weiter vereinfachen, um es einer breiteren Gruppe von Schaltungsentwicklern und Verifikationsingenieuren zugängig zu machen. Im Ergebnis wird angestrebt, die extremen Qualitätsmaßstäbe des Unternehmens bezüglich der Fertigung auch auf die Designebene auszuweiten.

 
Revision 14 Dec 2006