Automatisierte Verifikationstechniken bei unvollständiger Information

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.

Weitere Informationen: http://ira.informatik.uni-freiburg.de/src/projects_view.php?projectID=31

Projektbeginn: 2000
Projektende: (unbegrenzt)

Becker B

Albert-Ludwigs-Universität Freiburg
Rechnerarchitektur
Prof. Dr. Bernd Becker
Georges-Köhler-Allee 051
79110 Freiburg i. Br.

Telefon: 0761 203 8140
Fax: 0761 203 8142
http://ira.informatik.uni-freiburg.de

• Disch
• Herbstritt