DFG fördert Projekt: Wie rechnet ein Computer?
- Photo Info
- Download
Wie rechnet ein Computer? Arbeitsgruppe erforscht vollautomatischen Nachweis
Die Arbeitsgruppe Rechnerarchitektur im Fachbereich Mathematik / Informatik der Universität Bremen arbeitet gemeinsam mit der Albert-Ludwigs-Universität Freiburg an einem Projekt zum vollautomatisierten Nachweis arithmetischer Schaltkreise in Computern. Die Deutsche Forschungsgemeinschaft (DFG) fördert das Projekt über drei Jahre mit mehr als einer halben Million Euro.
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: grosse@informatik.uni-bremen.de
www.informatik.uni-bremen.de/agra/ger/index.php
Universität Bremen Hochschulkommunikation und -marketing Telefon: +49 421 218-60150 E-Mail: presse@uni-bremen.de Über die Universität Bremen: Leistungsstark, vielfältig, reformbereit und kooperativ - das ist die Universität Bremen. Rund 23.000 Menschen lernen, lehren, forschen und arbeiten auf dem internationalen Campus. Ihr gemeinsames Ziel ist es, einen Beitrag für die Weiterentwicklung der Gesellschaft zu leisten. Mit gut 100 Studiengängen ist das Fächerangebot der Universität breit aufgestellt. Als eine der führenden europäischen Forschungsuniversitäten pflegt sie enge Kooperationen mit Universitäten und Forschungseinrichtungen weltweit. Gemeinsam mit sieben Partnerinstitutionen gestaltet die Universität Bremen in den nächsten Jahren eine Europäische Universität. Das Netzwerk YUFE - Young Universities for the Future of Europe wird von der EU-Kommission gefördert. In der Region ist die Universität Bremen Teil der U Bremen Research Alliance. Die Kompetenz und Dynamik der Universität haben zahlreiche Unternehmen in den Technologiepark rund um den Campus gelockt. Dadurch ist ein bundesweit bedeutender Innovations-Standort entstanden - mit der Universität Bremen im Mittelpunkt.