Die Multiplikation von zwei Zahlen mag für Grundschulkinder eine einfache Aufgabe sein, für Computer ist sie jedoch, insbesondere bei großen Zahlen, äußerst rechenintensiv. Gerade wenn eine Berechnung sehr schnell erfolgen oder der Stromverbrauch möglichst gering ausfallen soll, werden nach diesen Kriterien optimierte Schaltkreise, sogenannte Multiplizierer, eingesetzt. Der Fokus der ausgezeichneten Arbeit mit dem Titel „PolyCleaner: Clean your Polynomials before Backward Rewriting to Verify Million-gate Multipliers“ liegt auf der Verifikation von Multiplizierern, also dem Nachweis der korrekten Funktion solcher Schaltkreise. Dieser konnte bisher nur für vergleichsweise kleine Bitbreiten und einfache Architekturen vollautomatisch realisiert werden.
Die Bremer Forschungsarbeit erlaubt es nun erstmalig, die Korrektheit von Multiplizierern mit mehr als einer Millionen Gattern nachzuweisen. Dafür erarbeiteten die Wissenschaftler der Universität Bremen und des DFKI-Forschungsbereichs Cyber-Physical Systems unter Leitung von Prof. Dr. Rolf Drechsler neue theoretische Erkenntnisse, die Alizera Mahzoon in dem Werkzeug „PolyCleaner“ implementierte. Das Werkzeug verwendet sogenannte Polynome – d.h. Summen, deren Terme aus numerischen Konstanten und Variablen bestehen – für die Darstellung der Verifikationsaufgabe. Allerdings führte die Verwendung von Polynomen bisher aufgrund zahlreicher redundanter Terme zu einer Speicherexplosion, also zu einem explosionsartig ansteigenden Speicherplatzbedarf. Dank PolyCleaner wird genau dies verhindert: Redundante und hundertausendfach auftretende Terme werden zunächst beseitigt, so dass anschließend der automatische Korrektheitsnachweis problemlos gelingt.
Zu den Autoren
Alireza Mahzoon ist Doktorand des Graduiertenkollegs „System Design“ (SyDe), das im Rahmen der Exzellenzinitiative an der Universität Bremen gefördert wird. SyDe ist eine Zusammenarbeit der Universität Bremen mit dem DFKI und dem Deutschen Zentrum für Luft- und Raumfahrt (DLR). Herr Mahzoon wird durch den Deutschen Akademischen Austauschdienst (DAAD) im Rahmen des „Graduate School Scholarship Programme“ gefördert. Dieses Programm ermöglicht es SyDe, zusätzliche Mittel gezielt zur Internationalisierung einzusetzen.
Alireza Mahzoon erhielt 2016 seinen Master in Electrical Engineering an der Universität Tehran. In seiner Promotion beschäftigt sich Herr Mahzoon mit der Verifikation und dem Debugging von arithmetischen Schaltkreisen.
Dr. Daniel Große promovierte summa cum laude im Jahr 2008 an der Universität Bremen. Er verblieb als Postdoc in der Arbeitsgruppe Rechnerarchitektur von Prof. Dr. Rolf Drechsler an der Universität Bremen. Im Jahr 2010 war er Vertretungsprofessor an der Albert-Ludwigs-Universität Freiburg. Von 2013 bis 2014 war er CEO des Startups solvertec. Seit 2015 ist er Senior Researcher an der Universität Bremen und dem DFKI sowie wissenschaftlicher Koordinator des Graduiertenkollegs SyDe. Herr Große hat mehr als 100 Arbeiten in begutachteten Konferenzen und Zeitschriften publiziert, darunter auch zwei Best Paper Awards auf den Konferenzen FDL 2007 und DVCon Europe 2018.
Prof. Dr. Rolf Drechsler erhält mit dieser Auszeichnung bereits zum zweiten Mal den Best Paper Award der ICCAD. Im Jahr 2013 ist er für seine zusammen mit Dr. Stefan Eggersglüß und Prof. Dr. Robert Wille verfasste Publikation „Improved SAT-based ATPC: More Constraints, Better Compaction“ geehrt worden.
Professor Drechsler, der zum Thema „Automatische Synthese und Verifikation im computergestützten Schaltkreisentwurf“ habilitierte, erhielt 2001 einen Ruf an die Universität Bremen. Neben seiner Tätigkeit als Hochschullehrer war er von 2008 bis 2013 auch als Konrektor für Forschung und wissenschaftlichen Nachwuchs tätig. Seit 2011 leitet er zudem den Forschungsbereich Cyber-Physical Systems des DFKI. Rolf Drechsler ist Mitglied in zahlreichen Gremien und Komitees. Im Jahr 2012 wurde er zum sogenannten „Term Member“ der Graduiertenschule „Electrical and Computer Engineering“ der Duke University in North Carolina (USA) ernannt. Seit Anfang 2014 ist er Mitherausgeber der IEEE-Zeitschrift „Transactions on Computer-Aided Design of Integrated Circuits and Systems“. Aktuell hat er eine Honorarprofessur an der Amity University Dubai inne. In Indien war er bereits von 2015 bis 2016 zwei Jahre Gastprofessor an der Eliteuniversität IIT Kharagpur. Weiterhin ist er Sprecher des Graduiertenkollegs SyDe, das er im Rahmen der Exzellenzinitiative an der Universität Bremen mitbegründet hat.