Einsatz von Verifikationstechniken unter Berücksichtigung unvollständiger Information
Zusammenfassung der Projektergebnisse
Technologische Fortschritte ermöglichen eine stetig steigende Integrationsdichte in der Chipherstellung. So bestehen heutige ASICS 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 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. 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 waren diese Methoden bisher fast ausschließlich darauf beschränkt, die Korrektheit auf der Basis einer vollständigen Beschreibung des Entwurfes nachzuweisen. Andererseits führen gerade erst spät im Designablauf entdeckte Fehler zu enorm hohen Kosten. Es ist deshalb in hohem Maße 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. Nachdem bisher dazu im industriellen Umfeld, wenn überhaupt, fast ausschließlich simulationsbasierte Methoden angewendet wurden, ermöglichen es die Resultate des Projektes jetzt, durch die Anwendung formaler Verifikationstechniken schon in frühen Phasen des Designablaufs eine wesentlich exaktere Fehlererkennung durchzuführen. Es wurden Techniken zur automatisierten (formalen) Verifikation bei unvollständiger Information entwickelt und erfolgreich erprobt. Diese Techniken sind darüber hinaus dazu geeignet, um bei fehlerhaften Designs eine Fehlerdiagnose durchzuführen. Die Fehlerdiagnose ermöglicht es dem Entwerfer, automatisch den möglichen Ort des Fehlers einzugrenzen, um eine Korrektur des Fehlers zu erleichtern. Schließlich sind die Methoden auch dazu geeignet, die Überprüfung von Eigenschaften einer Implementierung durch Ausblenden komplexer Teile (im Sinne einer Abstraktion) zu erleichtern.
Projektbezogene Publikationen (Auswahl)
- Approximate symbolic model checking for incomplete designs. In: Formal Methods in Computer-Aided Design, pages 290-305, Nov 2004, LNCS Volume 3312
T. Nopper and C. Scholl
- Approximate symbolic model checking for incomplete designs. In: Proceedings of IWLS2004, Temucula, USA, June 2004
T. Nopper, C. Scholl
- Filter Based Diagnosis for Multiple Design Errors. In: Proceedings of GI/ITG/GMM-Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen'', Kaiserslautern, Germany, February 2004
C. Scholl, M. Büche
- Improved Equivalence Checking for Error Diagnosis. In: 3rd Annual Formal Equivalence Verification Workshop, Agios Ioannis, Greece, March 2004
C. Scholl
- On the Impact of Structural Circuit Partitioning on SAT-based Combinational Circuit Verification. Int'l Workshop on Microprocessor Test and Verification pp.50-55 Austin (TX), USA, IEEE Computer Society
M. Herbstritt, T. Kmieciak, B. Becker
- Symbolic Model Checking for Incomplete Designs. Technical Report 201, Albert-Ludwigs-University, Freiburg, May 2004
T. Nopper, C. Scholl
- Flexible Modeling of Unknowns in Model Checking for Incomplete Designs. Proceedings of GI/ITG/GMM-Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen'', Munich, Germany, April 2005
T. Nopper, C. Scholl
- On SAT-based Bounded Invariant Checking of Blackbox Designs, Int'l Workshop on Microprocessor Test and Verification pp.23- 28, IEEE Computer Society
M. Herbstritt, B. Becker
- Advanced SAT-Techniques for Bounded Model Checking of Blackbox Designs. Int'l Workshop on Microprocessor Test and Verification, Austin (TX), USA, IEEE Computer Society, Dec 2006
M. Herbstritt, B. Becker, C. Scholl
- Advanced unbounded model checking by using AIGs, BDD sweeping and quantifier scheduling. Proceedings of Formal Methods in Computer-Aided Design, San Jose, USA, November 2006
F. Pigorsch, C. Scholl, S. Disch
- Advanced unbounded model checking by using AIGs, BDD sweeping and quantifier scheduling. Proceedings of GI/ITG/GMM-Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen'', Dresden, Germany, February 2006
F. Pigorsch, C. Scholl, S. Disch
- Combinational Equivalence Checking Using Incremental SAT Solving, Output Ordering, and Resets. Proceedings of the Asia and South Pacific Design Automation Conference, Yokohama, Japan, January 2007
S. Disch, C. Scholl
- Computation of Minimal Counterexamples by Using Black Box Techniques and Symbolic Methods. Proceedings of International Conference on Computer Aided Design (ICCAD), San Jose, USA, November 2007
T. Nopper, C. Scholl, B. Becker
- Counterexample Generation for Incomplete Designs. Proceedings of GI/ITG/GMM-Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen'', Erlangen, Germany, March 2007
T. Nopper, C. Scholl
