Student (m/w/d): Automatisierte Verifikation von Digitalschaltungsnetzlisten mittels z3
Während deines Studiums kannst du dich bei uns in laufende Forschungsprojekte einbringen. Geh mit uns an Grenzen des technisch Machbaren und sei dabei, wenn wir gemeinsam Neuland betreten. Wir bieten vielfältige herausfordernde und praxisorientierte Themen für Pflichtpraktika, Bachelor- bzw. Master-Arbeiten oder studentische Assistenztätigkeiten an. Du analysierst wichtige wissenschaftliche Vorlauffragestellungen und stehst den Projektteams mit unterstützenden Entwicklungstätigkeiten zur Seite.
Arbeitsort: Erfurt
Team: Mikroelektronik
Karrierestufe: Abschlussarbeit
Forschungsfeld: Integrierte Sensorsysteme
Umfang: nach Vereinbarung
Beginn: ab sofort
Bewerbungsfrist: 31.03.2026
Kennziffer: IMMS_STUD_ME_0226
Die Optimierung digitaler Schaltungen hinsichtlich Fläche und Performanz ist ein zentraler Prozess der Hardwareentwicklung. Am IMMS wird hierfür ein Python-Framework eingesetzt, das Netzlisten automatisiert analysiert und modifiziert, um bspw. Platz oder Energie zu sparen. Zur Sicherstellung der funktionalen Korrektheit nach solchen Modifikationen werden Logische Äquivalenzchecks (LECs) durchgeführt. Dabei werden Schaltungskonstrukte in mathematische Gleichungen transformiert, deren Gleichheit formal bewiesen oder widerlegt wird. Derzeit wird hierfür das Tool Yosys mit dem Plugin EQY genutzt. Aufgrund von Bugs in EQY und um die volle Kontrolle über den Workflow zu erhalten, soll eine maßgeschneiderte Alternative direkt in das Framework integriert werden. Das Ziel ist daher die Entwicklung eines LEC-Verfahrens auf Basis des SMT-Solvers z3 mittels dessen Python-API. Es soll ein systematisches Vorgehen erarbeitet werden, um Schaltungen in logische Ausdrücke zu überführen und diese mittels z3 auf Äquivalenz zu prüfen. Die Lösung soll anschließend implementiert und an Testbeispielen validiert werden.
DAS IST ZU TUN:
* Analyse des bestehenden Python-Frameworks zur automatisierten Netzlisten-Modifikation
* Erarbeitung eines Modells zur Transformation digitaler Schaltungsstrukturen in logische Gleichungen (Formalisierung)
* Entwurf und schrittweise Implementierung eines Äquivalenzprüfers unter Nutzung des SMT-Solvers z3
* Test und Evaluation des entwickelten Tools anhand von Beispielschaltungen
DAS BRINGST DU MIT:
* Fortgeschrittene Python-Kenntnisse
* Fortgeschrittene Kenntnisse von Digitalschaltungen
* Grundlegendes Verständnis über SMT-Solver
* Grundlegende Kenntnisse im Umgang mit Git
UND DAS SIND WIR:
Wir am IMMS stärken Unternehmen mit anwendungsorientierter Forschung und Entwicklung in der Mikroelektronik, Systemtechnik und Mechatronik und transferieren Ergebnisse der Grundlagenforschung in Anwendungen. Wir unterstützen Unternehmen, international erfolgreiche Innovationen für Gesundheit, Umwelt und Industrie auf den Weg zu bringen und begleiten sie von der Machbarkeitsstudie bis zur Serienreife.
WIR SIND GESPANNT AUF DICH!
Wir freuen uns, wenn du mit uns arbeiten willst.
Bewirb dich bitte nur einmal – für dein Lieblingsthema oder für das, das deinen Interessen am nächsten kommt. So können wir deine Bewerbung am schnellsten bearbeiten und auf dich zukommen. Wenn dich viele Themen interessieren, formuliere das gern in dein Anschreiben mit rein. Falls unsere aktuellen Vorschläge nicht passen sollten – schick uns bitte eine Initiativbewerbung mit deinem Themenwunsch.
DAS HABEN WIR ZU BIETEN:
* einen attraktiven Arbeitsplatz in einem modernen sehr gut ausgestatteten und industrienah agierenden Forschungsinstitut
* Arbeit direkt an der Schnittstelle zwischen Universität und Industrie
* Mitarbeit in einem flexiblen und kreativen Team und an innovativen herausfordernden Themen
Für die ausgeschriebenen Aufgaben und mit den vorhandenen Arbeitsbedingungen ist eine Bewerbung unabhängig vom Geschlecht und / oder von eventuellen körperlichen Behinderungen möglich. Wir fördern die berufliche Gleichstellung von Frauen und Männern. Wir fordern vor allem Frauen auf, sich zu bewerben. Da Frauen am IMMS unterrepräsentiert sind, werden sie bei gleicher Eignung, Befähigung und fachlicher Leistung vorrangig berücksichtigt.
Anschrift:
IMMS Institut für Mikroelektronik- und Mechatronik-Systeme gemeinnützige GmbH (IMMS GmbH)
Ehrenbergstraße 27
98693 Ilmenau
Deutschland
Kontakt: Eric Schäfer
Was andere sagen:
Folge uns: