FEST - Funktionale Verifikation von Systemen

| Beteiligte Mitarbeiter | Projektbeschreibung | Zielsetzung des Projekts | Struktur des Projekts |

Beteiligte Mitarbeiter
Arbeitsgruppen Rechnerarchitektur und Betriebssysteme
Christoph Scholl, Prof. Dr.
Florian Pigorsch, Dipl.-Inf.

Es handelt sich um ein im Rahmen der Förderinitiative Ekompass gestartetes Projekt, das vom Bundesministerium für Bildung und Forschung (BMBF) sowie durch die edacentrum GmbH unterstützt wird. Projektpartner sind neben der Albert-Ludwigs-Universität Freiburg die TU Darmstadt, Universität Frankfurt/Main, TU Ilmenau, Universität Kaiserslautern sowie die Universität Tübingen. Im Rahmen des Projektes werden Lösungen erforscht, die eine einheitliche Verifikation von SoCs (System On Chip) ermöglichen. Mit dem gewonnenen Forschungs-Know-How soll die Halbleiter-Industrie in Deutschland unterstützt werden, um die Kompetenz ihrer Entwurfsteams auch in Zukunft auf höchstem Niveau zu halten und neue, leistungsfähigere Verfahren in ihre Entwurfsplattformen zu integrieren. Der Freiburger Beitrag zum Projekterfolg besteht in der Untersuchung und Entwicklung von Black-Box-Techniken bei der Eigenschaftsprüfung.

Weitere Informationen finden sich auf der [ecacentrum Homepage].

Die Innovation in der Entwurfsmethodik steht in einem permanenten Wettbewerb mit den Verbesserungen in der Halbleitertechnologie. Um den Fortschritt zu gewährleisten, muss die Entwurfsproduktivität durch EDA-Innovationen in gleichem Maße erhöht werden, in dem sich auch die Qualität der Technologie steigert. Damit dies gelingen kann, hat das Bundesministerium für Bildung und Forschung den Ekompass-Förderkomplex ins Leben gerufen, durch den die entsprechenden Forschungs-Maßnahmen ermöglicht werden sollen.

Derzeit decken kommerzielle EDA-Tools den Bedarf an Verifikationsverfahren nicht ab - es bestehen also Entwurfslücken, die es zu schliessen gilt. Ein Übergang von der vielerorts immer noch überwiegend eingesetzten Simulation zu formalen Ansätzen ist angesichts der Komplexität heutiger Entwürfe dringend erforderlich. Nur auf diese Weise kann sichergestellt werden, dass Halbleiter-Bausteine wie SoCs keine Entwurfsfehler aufweisen.

In den vergangenen Jahren sind zahlreiche gute Ansätze erforscht worden. Eine systematische und methodische Vorgehensweise zur Verifikation von der Systemebene bis zur elektrischen Ebene fehlt jedoch bis heute. Hier setzt das Projekt

Funktionale Verifikation von Systemen (FEST)

an, in dessen Kontext die sechs Projektpartner neue Verifikationsmethoden auf unterschiedlichen Ebenen entwickeln und diese in ein Gesamtsystem integrieren. Die Vernetzung der unterschiedlichen Universitäten und der damit verbundene Austausch von Forschungsergebnissen trägt dazu bei, dass homogene, qualitativ hochwertige und Ebenen übergreifende Verifikationswerkzeuge entstehen.

Auf Systemebene werden Methoden zur Modellierung von Zeiteigenschaften untersucht. Diese sind in der Lage, das Verhalten des gesamten Systems zu überprüfen, bevor eine Implementierung erfolgt. Fokus der Projektarbeit ist zudem, einen einheitlichen Ansatz für HW-/SW-Verifikation zu erforschen, der die gemeinsame Behandlung von Hard- und Softwarekomponenten erlaubt. Dies ist ein wichtiges Vorhaben sowohl auf System- als auch auf Architekturebene. Auf letzterer sollen darüber hinaus auch verbesserte Verfahren zur Eigenschaftsprüfung entwickelt werden. Hierbei kommen Black-/Grey-Box-Techniken zum Einsatz, durch die Gegenbeispiele generiert und Fehler lokalisiert werden können. Auch die Leistungsfähigkeit der Verifikationsmethodik für digitale Blöcke wird deutlich gesteigert, und durch die Entwicklung eines Werkzeugs zur Mixed-Signal-Eigenschaftsprüfung ist man in der Lage, auch die Verifikationstechniken auf sehr tiefen Abstraktionsebenen zu verbessern.

Auf den unterschiedlichen Abstraktionsebenen sind Modellierungen notwendig, die als Grundlage dafür dienen, die zu entwickelnden Verifikationsverfahren anzuwenden. Entsprechend ist der Projektinhalt in zwei Arbeitspakete unterteilt:

1. Modellierung und Abstraktion
   
2. Methoden und Integration
   

Beide Arbeitspakete bestehen aus mehreren Aufgaben, beim ersten Paket Modellierung und Abstraktion sind dies:

1. Einheitliche Semantik für Hardware- und
   Software-Systeme und Eigenschaftsextraktion
   
2. Modelle für Mixed-Signal-Verifikation
   
3. Zeiteigenschaften und Restriktionen in Modellen
   
4. Abstrakte Modelle auf Architektur-Ebene
   
5. Modellgenerierung für die Blockverifikation
   

Die Aufgaben der Universität Freiburg sind im Bereich Methoden und Integration angesiedelt, der in folgende Aufgaben gegliedert ist:

1. Verifikation und Analyse
   
2. Verfeinerung von Zeitrestriktionen
   
3. Transformation von zeitbewerteten Modellen
   
4. Kompositionale Verifikation auf Architektur-Ebene
   
5. Algorithmen zur Verifikation von Mixed-Signal-Systemen
   
6. Black-Box-Techniken bei der Eigenschaftsprüfung
   

Für die letztgenannte Aufgabe verantwortlich, sorgt die Freiburger Arbeitsgruppe dafür, dass für die Eigenschaftsprüfung leistungsfähige Black-Box-Techniken zur Verfügung stehen. Dabei stehen zwei unterschiedliche Sichtweisen bzw. Verfahren im Blickpunkt:

• Black-Box-Techniken für Gegenbeispiele
  
• Fehlerlokalisierung bei der Eigenschaftsprüfung