DFG fördert Projekt: Wie rechnet ein Computer?

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.

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.

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.

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.