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.