Automatisierte Verifikationstechniken bei unvollständiger Information
| Beteiligte Mitarbeiter
| Kooperationspartner
| Projektbeschreibung | Zielsetzung des Projekts | Publikationen
|
| Lehrstuhl für Rechnerarchitektur | |
| Bernd Becker, Prof. Dr. | |
| Lehrstuhl für Betriebssysteme | |
| Christoph Scholl, Prof. Dr. | |
| Arbeitsgruppen Rechnerarchitektur und Betriebssysteme | |
| Stefan Disch, Dipl.-Inf. | |
| ehemalige Mitarbeiter Lehrstuhl für Rechnerarchitektur | |
| Marc Herbstritt, Dr. | |
|
| |
| Lehrstuhl für Betriebssysteme | |
| Tobias Nopper, Dipl.-Inf | |
| ehemaliger Mitarbeiter Arbeitsgruppe für Betriebssysteme | |
| Mathias Büche | |
Technologische Fortschritte ermöglichen eine stetig steigende Integrationsdichte in der Chipherstellung. So bestehen heutige ASICS u.U. aus bis zu 100 Millionen Transistoren. Neben dem eigentlichen Entwurf wird zunehmend der Nachweis seiner Korrektheit zu einer Herausforderung, die Kosten dafür machen teilweise mehr als die Hälfte der gesamten Entwurfskosten aus. Da durch reine Simulation zumindest bei größeren Systemen nur ein verschwindend geringer Bruchteil des Systemverhaltens erfasst werden kann, haben in den vergangenen 10 Jahren formale Methoden zum Beweis der Korrektheit von Schaltungen enorm an Bedeutung gewonnen. Kommerzielle Werkzeuge mit integrierten, automatisierten, formalen Verifikationsansätzen sind verfügbar und werden im industriellen Umfeld eingesetzt. Die Verfahren lassen sich im wesentlichen in drei Gebiete einordnen:
- Äquivalenztest kombinatorischer Schaltungen,
- Äquivalenztest sequentieller Schaltungen und
- Beweis von Eigenschaften sequentieller Schaltungen.
Während der kombinatorische Äquivalenztest auch auf sehr große Schaltungen mit mehreren Millionen Gattern anwendbar ist, zielt der sequentielle Äquivalenzvergleich bzw. die Eigenschaftsprüfung auf Beschreibungen auf der Modulebene mit bis zu 100,000 Gattern ab. Allerdings sind all diese Methoden zur Zeit noch fast ausschließlich darauf beschränkt, die Korrektheit auf der Basis einer vollständigen Beschreibung des Entwurfes nachzuweisen. Andererseits führen erst spät im Designablauf entdeckte Fehler zu enorm hohen Kosten. Es ist deshalb erstrebenswert, schon möglichst früh, d.h. auch zu einem Zeitpunkt, wenn nur unvollständige Information über den Gesamtentwurf zur Verfügung steht, Maßnahmen zu einer möglichst vollständigen Entdeckung schon vorhandener Fehler zu ergreifen.
Bisher werden dazu im industriellen Umfeld, wenn überhaupt, fast ausschließlich simulationsbasierte Methoden angewendet. Erste Resultate zeigen, dass durch die Anwendung von formalen Verifikationstechniken schon in frühen Phasen des Designablaufs vermutlich eine wesentlich exaktere Fehlererkennung möglich ist. Es sollen deshalb Techniken zur automatisierten (formalen) Verifikation bei unvollständiger Information entwickelt und erprobt werden auf den Gebieten kombinatorischer Äquivalenztest, Äquivalenztest für sequentielle Schaltungen und Eigenschaftsprüfung von sequentiellen Schaltungen.
Diese Techniker sollen auch dazu angewendet werden, um bei fehlerhaften Designs eine Fehlerdiagnose durchzuführen. Die Fehlerdiagnose soll es dem Entwerfer ermöglichen, automatisch den möglichen Ort des Fehlers einzugrenzen, um eine Korrektur des Fehlers zu erleichtern.
Die Ziele des Projektes sind:
- Weiterentwicklung der Ansätze des kombinatorischen Äquivalenztests
- Äquivalenztests für Sequentielle Schaltungen bei unvollständiger Information
- Beweis von Eigenschaften sequentieller Schaltungen bei unvollständiger Information
|
C. Scholl, B. Becker Checking Equivalence for Circuits Containing Incompletely Specified Boxes |
|
C. Scholl, B. Becker Checking Equivalence for Partial Implementations |
|
T. Nopper, C. Scholl Approximate Symbolic Model Checking for Incomplete Designs |