PolyVer: Polynomiale Verifikation elektronischer Schaltungen

• Antragsteller: Professor Dr. Rolf Drechsler
• Fachliche Zuordnung: Rechnerarchitektur, eingebettete und massiv parallele Systeme
• Förderung: Förderung seit 2020
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 431649366

Die digitale Revolution hat unser Leben dramatisch verändert. Nach PCs, Internet und modernen mobilen Geräten hält die Digitalisierung in viele traditionelle Industrien Einzug. Die Grundlage dieser Revolution sind digitale Logikschaltungen. Damit diese all ihre wichtigen Aufgaben erfüllen können, müssen die Schaltkreise fehlerfrei arbeiten.Das Ziel des Projekts PolyVer ist es, den Nutzen von formalen Verifikationstechniken drastisch zu erhöhen, d.h. diese sollen zum "Schweizer Taschenmesser" für die Verifikation digitaler Schaltungen aus der Praxis werden. Dazu wird PolyVer den heutigen entwurfsorientierten Entwicklungsprozess von Schaltungen radikal verändern, d.h. in einem verifikationszentrierten Prozess transformieren. Dies soll durch einen auf den ersten Blick unmöglich zu erreichenden Ansatz möglich werden: formale Verifikation in polynomialer Zeit und Platz. Mit PolyVer werden formale Garantien, d.h. Nachweise im mathematischen Sinne, für heutige und zukünftige elektronische Systeme in vorhersehbarer Zeit Realität. Um dieses Ziel zu erreichen, wird PolyVer die theoretischen Grundlagen schaffen, indem ein feingranulares Verständnis der handhabbaren Schaltungsklassen entwickelt wird. Darauf aufbauend werden effiziente (d.h. polynomiale) Entscheidungsprozeduren für jede Schaltungsklasse einschließlich ihrer Komposition untersucht. Die wichtigsten Ergebnisse des Projekts sind neben den theoretischen Resultaten eine Reihe von effizient implementierten Verifikationsalgorithmen für die Schaltungsklassen, ihre Integration in einen durchgängigen und verifikationszentrierten Ablauf, sowie eine Reihe von Fallstudien zur Demonstration der Vorteile der polynomialen Verifikation.

• DFG-Verfahren: Reinhart Koselleck-Projekte