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 vollautomatisierte 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. 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.
Sprache der Kurzfassung:
Deutsch
Englische Bezeichnung:
VerA: Fully Automatic Formal Verification of Arithmetic Circuits
Englische Kurzfassung:
Today arithmetic circuits play a crucial role in many computationally intensive applications (like signal processing and cryptography) as well as in upcoming AI architectures (e.g. for machine learning and deep learning). The diversity of arithmetic circuits is huge and covers a wide range of different operations from trigonometric functions to floating point square root. Despite this diversity, almost all intricate operations can be performed using four basic operations: addition, subtraction, multiplication, and division. In order to satisfy the demands for high speed, low power, and low area designs, a large variety of architectures have been proposed for arithmetic units. These architectures take advantage of sophisticated algorithms to optimize different implementation aspects. As a result, they are usually extensively parallel and structurally complex which makes it extremely challenging to ensure the correctness of such arithmetic circuit implementations. In the project VerA, we envision a fully automatic formal verification methodology that goes beyond incomplete simulation-based approaches and semi-automatic approaches based on theorem proving which are still the state-of-the-art for arithmetic circuit verification in industrial practice. In this project, we focus on the most challenging task in arithmetic circuit verification, the verification of circuits containing complex and highly optimized industrial multipliers and dividers at the gate level. Whereas the question has been open for a long time, encouraged by recent advances in verification based on Symbolic Computer Algebra, we strongly believe that it is the ideal time to attack this problem.