Formale Verifikation von Multiplizierern mit Computeralgebra

Abstract

Arithmetische Schaltungen werden in Prozessoren zur Implementierung von Boolescher Algebra genutzt. Aufgrund des weitreichenden Einsatzes von Prozessoren ist es äußerst wichtig, die Korrektheit dieser Schaltungen garantieren zu können, um Fehler wie den beru ̈hmten Pentium FDIV- Bug zu vermeiden. Mithilfe formaler Verifikation kann festgestellt werden, ob eine Schaltung ihrer gewünschten Spezifikation entspricht. Allerdings stellen arithmetische Schaltungen, insbesondere Integer-Multiplizierer auf Gatterebene, eine Herausforderung für bestehende Verifikationstechniken dar. In dieser Dissertation [Ka20] werden aktuelle Verifikationsmethoden basierend auf Computeral- gebra verbessert. Wir zeigen eine rigorose präzise mathematische Formulierung, welche auch die Anwendung der Mathematik in diesem Gebiet erweitert. Außerdem haben wir neue Methoden zur vollautomatischen Verifikation von Integer-Multiplizierern entworfen und implementiert, sowie ein kompaktes Beweisformat entwickelt, um das Ergebnis der Verifikation zertifizieren zu können.