Hierarchische und sequentielle Informationen für Erfüllbarkeitsbeweise im computergestützten Schaltkreisentwurf

In diesem Projekt sollen Methoden zur Ausnutzung sequentieller und hierarchischer Information beim Lösen von Instanzen des Booleschen Erfüllbarkeitsproblems (Boolean Satisfiability) erarbeit und an praktischen Problemstellungen aus Test, Verifikation und Diagnose evaluiert werden.

Kontakt: Prof. Dr. Rolf Drechsler

Integrierte Schaltkreise und Systeme finden immer breitere Anwendung auch in sicherheitskritischen Bereichen. Die ständig wachsende Komplexität dieser Systeme führt zu steigenden Herstellungskosten. Einen großen Anteil daran haben der Nachweis der Korrektheit eines Entwurfs - die Verifikation - und die Überprüfung eines gefertigten Schaltkreises - der Test. In beiden Bereichen werden Algorithmen zur Lösung Boolescher Erfüllbarkeit (SAT), deren Performanz in den vergangenen Jahren deutlich stieg, häufig eingesetzt.
In der Zusammenarbeit mit der Arbeitsgruppe aus Toronto sollen Methoden untersucht werden, um sequentielle sowie hierarchische Probleme, wie sie in Verifikation und Test von Schaltkreisen auftreten, effizient durch SAT-Beweiser zu lösen. Im Vordergrund steht dabei die Frage, wie hierarchische und sequentielle Informationen, die aus der ursprünglichen Problemstellung zur Verfügung stehen, im SAT-Beweiser zur Performanzsteigerung ausgenutzt werden können.