Uni-Logo
English       Login
Professur für Betriebssysteme
        Startseite         |         Institut für Informatik         |         Technische Fakultät
 

VerA: Vollautomatische Formale Verifikation Arithmetischer Schaltkreise

| Beteiligte Mitarbeiter | Kooperationspartner | Projektbeschreibung | Software | Publikationen |


Beteiligte Mitarbeiter

Lehrstuhl für Betriebssysteme
Alexander Konrad
Christoph Scholl, Prof. Dr.
Kooperationspartner

Universität Bremen
Alireza Mahzoon, Dr.
Rolf Drechsler, Prof. Dr.
Johannes Kepler Universität Linz
Daniel Große, Prof. Dr.


Projektbeschreibung

Arithmetische Schaltkreise spielen heute eine wesentliche Rolle in zahlreichen rechenintensiven Anwendungen (wie z.B. Signalverarbeitung und Kryptographie) sowie in künftigen KI-Architekturen (z.B. für Maschinelles Lernen und Deep Learning). Es gibt eine Vielzahl von arithmetischen Schaltkreisen, die ein breites Spektrum abdecken von trigonometrischen Funktionen bis zum Wurzelziehen für Fließkommazahlen. Trotz dieser Diversität können fast alle dieser komplexen Operationen auf vier Grundoperationen zurückgeführt werden: Addition, Subtraktion, Multiplikation und Division. Um die gestellten Anforderungen hinsichtlich Geschwindigkeit, Leistungsverbrauch und Fläche der Entwürfe erfüllen zu können, sind eine Vielzahl von Architekturen vorgeschlagen worden. Diese Architekturen nutzen ausgefeilte Algorithmen, um verschiedene Implementierungsaspekte zu optimieren. Dadurch sind sie in der Regel stark parallelisiert und strukturell komplex, so dass es eine immense Herausforderung darstellt, die Korrektheit solcher Implementierungen arithmetischer Schaltungen zu gewährleisten.

Im Projekt VerA schlagen wir eine voll automatisierte formale Methodik zur Verifikation vor, die weit über unvollständige simulationsbasierte Ansätze sowie halbautomatische Ansätze basierend auf Theorembeweisern hinaus geht, die nach wie vor den Stand der Technik bei der Verifikation arithmetischer Schaltkreise in der Industrie darstellen. Nur *formale* Verifikation ist in der Lage, strikte Korrektheitsgarantien für arithmetische Schaltkreise zu liefern. *Vollautomatische* Verfahren werden benötigt, da sich der Entwurf von Schaltkreisen mit arithmetischen Komponenten heutzutage nicht mehr nur auf die größeren Prozessorhersteller beschränkt, sondern ebenso von vielen unterschiedlichen Anbietern eingebetteter Spezial-Hardware durchgeführt wird. Diese können sich häufig die Beschäftigung großer Teams spezialisierter Verifikationsingenieure nicht leisten, die in der Lage sind, halbautomatische Theorembeweise zu führen. Zusammenfassend ist festzustellen, dass der Bedarf für die vollautomatische formale Verifikation arithmetischer Schaltkreise in den letzten Jahren enorm gestiegen ist.

In diesem Projekt legen wir unseren Hauptaugenmerk auf die größte Herausforderung bei der Verifikation arithmetischer Schaltungen, nämlich die Verifikation von Schaltungen, die komplexe und hochoptimierte industrielle Multiplizierer und Dividierer auf Gatterebene enthalten. Während diese Problemstellung schon lange Zeit offen ist, sind wir - ermutigt durch die jüngsten Fortschritte bei der Verifikation basierend auf symbolischer Computeralgebra - der festen Überzeugung, dass aktuell der ideale Zeitpunkt ist, um das Problem anzugehen.



Software

FMCAD 22 Tools and Benchmarks

The binaries have been compiled and tested on Ubuntu 20.04 LTS.



Publikationen
Christoph Scholl, Alexander Konrad
Symbolic Computer Algebra and SAT Based Information Forwarding for Fully Automatic Divider Verification
2020 57th ACM/IEEE Design Automation Conference (DAC)
Alexander Konrad, Christoph Scholl, Alireza Mahzoon, Daniel Große, Rolf Drechsler
Verifying Dividers Using Symbolic Computer Algebra and Dont Care Optimization
2021 Design, Automation & Test in Europe Conference & Exhibition (DATE)