Computer sind allgegenwärtig. So begleitet uns das Smartphone durch den Tag, wenn wir Musik hören, unsere Termine verwalten oder uns morgens wecken lassen. Egal, ob wir Filme anschauen oder ob eine Künstliche Intelligenz uns gezielt Informationen zur Verfügung stellt, im Inneren der Maschine wird alles mit sehr einfachen Befehlen abgebildet. Mehrere Millionen dieser Befehle können gleichzeitig pro Sekunde ausgeführt werden. Dabei spielt die Arithmetik die zentrale Rolle: Wie schon in der Schule vermittelt wird, sind plus, minus, mal und geteilt die Grundlage für alle komplexen Berechnungen.

Damit diese Operationen in einem Computer sehr schnell, aber zugleich auch auf geringem Raum und noch dazu mit wenig Energieverbrauch realisiert werden können, wurden in den vergangenen Jahren neue Architekturen entwickelt. „Dabei wird nicht eine Berechnung nach der anderen durchgeführt, sondern es wird hochparallel gearbeitet“, erläutert Professor Rolf Drechsler, der das Projekt an der Universität Bremen leitet. Berechnungen in der Maschine würden dadurch aber schwer nachvollziehbar und die Korrektheit des Gesamtsystems sei nicht offensichtlich.

Statt von Hand nun vollautomatisiert

In dem von der Deutschen Forschungsgemeinschaft (DFG) mit mehr als einer halben Million Euro geförderten Projekt zur Verifikation von Arithmetik-Schaltkreisen (VerA) wird eine vollautomatisierte formale Methodik zum Nachweis entwickelt. Das Resultat ist vergleichbar zu einem von einem Menschen durchgeführten Beweis per Hand, nur dass in diesem Fall die Beweisführung vollautomatisch durch ein Computerprogramm übernommen wird. Dies geht weit über die Ansätze hinaus, die bisher in der Industrie verwendet werden.

Wichtig auch für den Mittelstand

Vollautomatisierte Verfahren werden insbesondere deshalb benötigt, weil sich der Einsatz von Schaltkreisen mit arithmetischen Komponenten heutzutage nicht mehr nur auf die größeren Prozessorhersteller beschränkt. Sie werden auch von Anbietern mit eingebetteter Spezial-Hardware im Mittelstand genutzt. Diese können sich häufig große Teams spezialisierter Testingenieurinnen und -ingenieure nicht leisten. Durch die DFG-Förderung ist es nun möglich, für dieses seit langer Zeit bekannte Problem vollautomatische Lösungen zu erarbeiten.

Wesentliche Vorarbeiten in Bremen

Schon viele Jahre beschäftigt sich die Arbeitsgruppe Rechnerarchitektur in Bremen mit der Korrektheit von Schaltungen. 2018  hat sie den Nachweis für große Multiplizierer erbracht, was wesentliche Vorarbeiten zum jetzt geförderten Projekt darstellte. Die zugehörige Forschungsarbeit wurde im November 2018 mit dem Best Paper Award auf der International Conference on Computer Aided Design (ICCAD), einer der führenden Tagungen auf dem Gebiet des Schaltkreisentwurfs, ausgezeichnet. An diese Ergebnisse knüpft nun das Projekt VerA an und fokussiert auf die vollautomatische Verifikation von industriellem Multiplizieren und Dividieren.

Beteiligte Wissenschaftler:

An dem erfolgreichen DFG-Antrag waren die folgenden Wissenschaftler beteiligt: Prof. Dr. Rolf Drechsler und Dr.-Ing. Daniel Große von der Universität Bremen sowie Prof. Christoph Scholl von der Albert-Ludwigs-Universität Freiburg.

Fragen beantworten:

Universität Bremen
Fachbereich Mathematik/Informatik
Arbeitsgruppe Rechnerarchitektur
Dr. Daniel Große/Prof. Dr. Rolf Drechsler
Telefon: +49-421-218-63935

E-Mail: grosseprotect me ?!informatik.uni-bremenprotect me ?!.de
www.informatik.uni-bremen.de/agra/ger/index.php