2009
Formale Verifikation eines komplexen Bussystems für mehrere Prozessoren und Speicherblöcke einer Software-Defined-Radio Plattform von Infineon: Neubiberg bei München, 3 Monate
- Einarbeitung in VHDL Design und bereits vorliegender Verifikationseigenschaften eines Verifikationsteams
- Fertigstellen der vollständigen Verifikation von zwei Modulen des Bussystems
- Werkzeuge: Onespin, Debussy, ClearCase
2008
Weiterentwicklung der Methodik zur vollständigen Verifikation industrieller Designs mit OneSpin: München, 2 Monate
- Aufstellen von Designregeln zur Vereinfachung der Erreichbarkeitsanalyse
- Systematische Durchführung von Erreichbarkeitsanalysen
2007
Formale Verifikation eines Memory-Controllers mit OneSpin: München, 5 Wochen
- Eigenverantwortlicher Nachweis einiger essentieller Invarianten des Controllers
- Entwicklung der Eigenschaften und deren Verifikation für unterschiedliche Arten von Speicherzugriffen nach dem AMBA AHB Standard in Zusammenarbeit mit einem zweiten Verifikationsingenieur
- Analyse der Ursache gefundener funktionaler Entwurfsfehler und Herleitung von Designkorrekturen
- Zusammenführen der entwickelten Eigenschaften und Nachweis der Vollständigkeit der Verifikation
- Werkzeuge: Onespin, Debussy, CVS
2006 - 2007
Formale Verifikation am TriCore Prozessor von Infineon mit OneSpin: München, 8 Monate
- Innerhalb eines Teams aus 4 Personen verantwortlich für die Entwicklung der Verifikationseigenschaften für eine Gruppe von multi-cycle Assembler Befehlen und deren Verifikation
- Analyse der parallelen Ausführung der Assembler Befehle durch die Prozessor-Pipeline anhand des VHDL-Codes
- Zusammenführen der entwickelten Eigenschaften von mehreren Teilen des Prozessors
- Nachweis der Vollständigkeit der Verifikation
- Projektübergabe an die Entwickler in Bristol / England
- Werkzeuge: Onespin, Debussy, CVS
2006
Weiterentwicklung der Methodik zur vollständigen Verifikation industrieller Designs mit OneSpin: München, 5 Monate
- Planung von Verifikationsaufgaben von der Durchsicht des VHDL/Verilog Codes bis zur Vollständigkeitsprüfung
- Untersuchung von multi-cycle Befehlen
2005
Formale Verifikation an einem Controller für die Telekommunikation mit gateprop: Xian / China, 2 Monate
- Einarbeitung in ein bestehendes Design mit Hilfe der Entwickler vor Ort und Festlegung der formal zu verifizierenden kritischen Operationen
- Eigenverantwortliche formale Verifikation mit gateprop
- Analyse der Ursache gefundener funktionaler Entwurfsfehler und Herleitung von Designkorrekturen
- Werkzeuge: gateprop, ClearCase
1999 - 2004
Festanstellung als Wissenschaftlicher Mitarbeiter am Fachgebiet Rechnersysteme der TU Darmstadt:
- Eigenverantwortliche objektorientierte Planung und Implementierung einer Software in C++ zum automatischen Beweisen von Assertions/Invarianten von Hardware-Designs, 3 Jahre
- Parsen einfacher HDL-Beschreibungen mit flex/bison
- Automatische Generierung von verstärkenden Assertions nach einer selbst entwickelten Methode bis zum induktiven Beweis der Invarianten
- Formale Verifikation mit gateprop: Kooperation mit der Siemens AG und der Infineon AG in München, 6 Monate
- UART: Senden und Empfangen von Daten, Interrupts, DMA
- Microcontroller Bus-Interface: Formale Verifikation von Speicherzugriffen
- Bus-Controller: Verifikation der Arbitrierung, Ausschluss von Buskollisionen
- DMA-Controller: Verifikation einiger Corner-Cases
- Tätigkeit in der Lehre zur Ausbildung von Studenten im Hauptstudium der Datentechnik, 2 Jahre
- Starke Erweiterung und Vertiefung meiner Kenntnisse in folgenden Bereichen:
- Verschiedene Konzepte von Rechner-/Prozessorarchitekturen und Pipelines für daten-/kontrollintensive Anwendungen
- Optimierende Compiler-Techniken für Prozessoren mit Pipeline, auch superskalar
- Speicherhierarchien, Cache-Organisation, virtueller Speicher
- Multiprozessor-Techniken, Shared-Memory, Bussysteme
- Echtzeitplanung
1994 - 1998 als Werkstudent, ca. 1 Jahr
1998 - 1999 in Festanstellung, 1 Jahr
Entwicklung von Software zur Daten- und Programmanalyse mit Logikanalysatoren:
- Eigenverantwortliche Inbetriebnahme von Evaluation-Boards einzelner Prozessoren/Microcontroller von Motorola/Freescale: Erstellen von Testprogrammen in der jeweiligen Assembler-Sprache und Erfassung der Prozessorsignale mit dem Logikanalysator in Echtzeit
- Entwicklung von Software in C/C++ zur Analyse der aufgezeichneten Rohdaten und anschließende Disassemblierung
- Objektorientierte Entwicklung von Software in C++ zur Verknüpfung aufgezeichneter Rohdaten aus Programmen einer Hochsprache mit den Programmzeilen des ursprünglichen Quellcodes durch Analyse der Debuginformation aus dem ELF/DWARF Format
- Messgeräte: DLI Logikanalysatoren Personal Line und Pro Line
- Datenformate: ELF, DWARF