VerA: Vollautomatische Formale Verifikation Arithmetischer Schaltkreise

• Antragsteller: Professor Dr. Rolf Drechsler; Professor Dr.-Ing. Daniel Große; Professor Dr.-Ing. Christoph Scholl
• Fachliche Zuordnung: Rechnerarchitektur, eingebettete und massiv parallele Systeme
• Förderung: Förderung von 2020 bis 2024
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 436285168

• Erstellungsjahr: 2025

Zusammenfassung der Projektergebnisse

Das Projekt startete ausgehend von der Beobachtung, dass aktuell arithmetische Schaltungen in vielen rechenintensiven Anwendungen (wie z.B. Signalverarbeitung und Kryptographie) sowie in kommenden KI-Architekturen (z.B. für das Maschinelle Lernen und Deep Learning) eine wesentliche Rolle spielen, dass aber nichtsdestotrotz die Verifikation arithmetischer Schaltungen nach wie vor eine große Herausforderung für automatische Verifikationstechnologien darstellte – obwohl spätestens seit dem berühmten Pentium-Bug im Jahr 1994 schon beträchtliche Forschungsanstrengungen in die Verifikation arithmetischer Schaltungen geflossen waren. Unser Hauptziel war es, eine vollautomatische formale Verifikationsmethodik zu entwickeln, die über unvollständige simulationsbasierte Ansätze sowie halbautomatische Ansätze auf der Basis von Theorembeweisern hinausgeht, die in der industriellen Praxis immer noch den Stand der Technik für die Verifikation arithmetischer Schaltungen darstellen. Nur die formale Verifikation ist in der Lage, strikte Garantien für die Korrektheit arithmetischer Schaltungen zu geben. Eine vollständige Automatisierung ist erforderlich, da der Entwurf von (anwendungsspezifischen) Schaltungen, die Arithmetik enthalten, heutzutage nicht mehr nur auf die großen Prozessorhersteller beschränkt ist, sondern auch von vielen verschiedenen Anbietern eingebetteter Hardware durchgeführt wird, die es sich nicht leisten können, große Teams spezialisierter Verifikationsingenieure zu beschäftigen, die in der Lage sind, interaktive Theorembeweise liefern. Die vollständige Automatisierung ermöglicht es auch Nicht-Fachleuten, die Verifikation von arithmetischen Schaltungen durchzuführen. In diesem Projekt konnten wir den Stand der Technik bei der vollautomatischen formalen Verifikation von Multiplizierern und Dividierern einen entscheidenden Schritt voranbringen. Unsere Arbeit baut auf neueren Fortschritten in der Anwendung Symbolischer Computeralgebra (SCA) für die Verifikation arithmetischer Schaltungen auf. Mit einer Reihe von Verbesserungen wie z.B. effizienten Datenstrukturen für Polynome, neuartigen Minimierungsmethoden für Polynome und verbesserten Konstruktionsmethoden für Polynome konnten wir eine hochgradig robuste und vollautomatische formale Verifikationsmethode für große, komplexe und stark optimierte Multiplizierer liefern. Auch die Verifikation von Dividierern konnten wir erfolgreich in Angriff nehmen. Hier konnten wir zeigen, dass die Verifikation von Dividierern nicht allein mit SCA- basierten Methoden durchgeführt werden kann, die im Wesentlichen ausgehend von einem Spezifikationspolynom die Signale der Schaltung in umgekehrter topologischer Reihenfolge durch Polynome für die entsprechenden Gatter ersetzen. Für eine erfolgreiche Verifikation von großen Dividerern muss eine solche SCA-basierte Konstruktionsmethode zwingend ergänzt werden durch Vorwärtspropagation von Information von den Eingängen in Richtung der Ausgänge. Auf der Grundlage dieser Erkenntnis und einer Reihe von Optimierungsmethoden waren wir schließlich in der Lage, (vollautomatische) Korrektheitsbeweise für große Dividierer zu liefern, die nicht-triviale Optimierungen auf Architekturebene enthalten.

Projektbezogene Publikationen (Auswahl)

• Symbolic Computer Algebra and SAT Based Information Forwarding for Fully Automatic Divider Verification. 2020 57th ACM/IEEE Design Automation Conference (DAC), 1-6. IEEE.
  Scholl, Christoph & Konrad, Alexander
  
• Towards Formal Verification of Optimized and Industrial Multipliers. 2020 Design, Automation & Test in Europe Conference & Exhibition (DATE), 544-549. IEEE.
  Mahzoon, Alireza; Grose, Daniel; Scholl, Christoph & Drechsler, Rolf
  
• GenMul: Generating Architecturally Complex Multipliers to Challenge Formal Verification Tools. Recent Findings in Boolean Techniques, 177-191. Springer International Publishing.
  Mahzoon, Alireza; Große, Daniel & Drechsler, Rolf
  
• Verifying Dividers Using Symbolic Computer Algebra and Don't Care Optimization. 2021 Design, Automation & Test in Europe Conference & Exhibition (DATE), 1110-1115. IEEE.
  Scholl, Christoph; Konrad, Alexander; Mahzoon, Alireza; Grobe, Daniel & Drechsler, Rolf
  
• Divider verification using symbolic computer algebra and delayed don’t care optimization. In Int’l Conf. on Formal Methods in CAD, pages 108–117
  Alexander Konrad, Christoph Scholl, Alireza Mahzoon, Daniel Große & Rolf Drechsler
  
• Formal verification of modular multipliers using symbolic computer algebra and boolean satisfiability. Proceedings of the 59th ACM/IEEE Design Automation Conference, 1183-1188. ACM.
  Mahzoon, Alireza; Große, Daniel; Scholl, Christoph; Konrad, Alexander & Drechsler, Rolf
  
• RevSCA-2.0: SCA-Based Formal Verification of Nontrivial Multipliers Using Reverse Engineering and Local Vanishing Removal. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 41(5), 1573-1586.
  Mahzoon, Alireza; GroBe, Daniel & Drechsler, Rolf
  
• Formal Verification of Structurally Complex Multipliers. Springer International Publishing.
  Mahzoon, Alireza; Große, Daniel & Drechsler, Rolf
  
• Divider verification using symbolic computer algebra and delayed don’t care optimization: theory and practical implementation. Formal Methods in System Design, 67(1), 106-142.
  Konrad, Alexander; Scholl, Christoph; Mahzoon, Alireza; Große, Daniel & Drechsler, Rolf
  
• Symbolic computer algebra for multipliers revisited - it’s all about orders and phases. In Int’l Conf. on Formal Methods in CAD, 2024
  Alexander Konrad & Christoph Scholl