Formaler Robustheitsnachweis im computergestützten Schaltkreisentwurf

• Antragsteller: Professor Dr. Rolf Drechsler
• Fachliche Zuordnung: Rechnerarchitektur, eingebettete und massiv parallele Systeme
• Förderung: Förderung von 2008 bis 2012
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 61273444

Es wird zunehmend wichtiger, dass integrierte Schaltkreise selbst beim Auftreten interner Fehlfunktionen noch ein korrektes Ein- /Ausgabeverhalten zeigen. Doch der Nachweis dieser Robustheit gegenüber Fehlern wird bisher für den industriellen Schaltkreisentwurf nicht ausreichend unterstützt. Üblicherweise werden derzeit simulationsbasierte Methoden für den Nachweis der Robustheit eingesetzt. Dabei wird aber keine ausreichende Überdeckung des Zustandsraumes eines Schaltkreises erreicht. Formale Methoden können dagegen Robustheit unter allen Zuständen garantieren. Im beantragten Projekt sollen Ansätze zum Robustheitsnachweis von Schaltkreisen unter Verwendung formaler Methoden erarbeitet werden. Erste viel versprechende Vorarbeiten hierzu wurden bereits durchgeführt. Hierbei wurden erste Lösungsansätze implementiert, deren Effizienz jedoch noch nicht für die praktische Anwendung ausreicht. Außerdem wurden weiterführende Fragestellungen bezüglich der Behandlung unterschiedlicher Fehlertypen identifiziert. Deshalb sollen die vorhandenen Ansätze im beantragten Projekt weiterentwickelt und anhand praktischer Beispiele evaluiert werden. Das Projektziel ist die Entwicklung eines vollautomatischen Werkzeuges zur Klassifikation der Robustheit eines Schaltkreises. Die zugrunde liegenden Beweismethoden sollen für den Nutzer transparent sein, so dass das Werkzeug einfach zu bedienen ist.Gleichzeitig soll es möglich sein auch große Schaltkreise mit den erarbeiteten Werkzeugenbearbeiten zu können.

• DFG-Verfahren: Sachbeihilfen
• Beteiligte Person: Professor Dr.-Ing. Görschwin Fey