« zurück

Erfolgreiche Verteidigung der Dissertation

Dr. Amr Sayed-Ahmed

In seiner Dissertation „Highly Automated Formal Verification of Arithmetic Circuits” erarbeitete Dr. Amr Sayed-Ahmed eine vollautomatische Methode für die formale Verifikation von arithmetischen Schaltkreisen. Dabei fokussierte er insbesondere auf Multipliziererschaltkreise für Ganze Zahlen und Gleitkommazahlen. Die neu entwickelten Verfahren basieren auf Methoden der Computer Algebra. Dabei werden Polynomdarstellungen zur Repräsentation der Logikgatter eingesetzt und die Korrektheit eines Schaltkreises kann auf das Lösen des Idealzugehörigkeitstests erbracht werden. Die zentralen Ergebnisse seiner Doktorarbeit sind einerseits das Einbringen lokaler Logikoptimierungen in die algebraischen Methoden und andererseits eine algebraisches Verfahren zum Nachweis der Äquivalenz zweier Schaltungen. Im Gegensatz zu existierenden Verfahren ist es somit erstmals möglich die Korrektheit großer Multiplizierer vollautomatisch zu beweisen.

Wir gratulieren!