Formale Verifikation mit Decision Diagrams
| Beteiligte Mitarbeiter | Projektbeschreibung | Publikationen
|
| ehemaliger Mitarbeiter Lehrstuhl ür Rechnerarchitektur | |
| Wolfgang Günther, Dr. | |
| Rolf Drechsler, Prof. Dr. | |
| Marc Herbstritt, Dr. | |
Die formale Verifikation beschäftigt sich damit, für ein gegebenes Design die Korrektheit zu beweisen. Dabei kann die Spezifikation auf verschiedenen Abstraktionsebenen gegeben sein. In vielen Fällen werden zur Verifikation BDDs als zugrundeliegende Datenstruktur verwendet. Für Multiplizierer haben BDDs jedoch unter allen Variablenordnungen exponentielle Größe. Um dieses Problem zu umgehen weden oft Word Level Decision Diagrams wie BMDs oder K*BMDs eingesetzt. Die für BDDs eingesetzten unteren Schranken konnten für K*BMDs übertragen werden.
|
Rolf Drechsler, Prof. Dr., Bernd Becker, Prof. Dr., Stefan Ruppertz K*BMDs: A New Data Structure for Verification IEEE Design & Test Conference, 1996 |
|
Stefan Höreth , Rolf Drechsler, Prof. Dr. Dynamic Minimization of Word-Level Decision Diagrams Design, Automation and Test in Europe, 1998 |
|
S. Höreth, Rolf Drechsler, Prof. Dr. Formal Verification of Word-Level Specifications Design, Automation and Test in Europe, 1999 |
|
Rolf Drechsler, Prof. Dr., Marc Herbstritt, Dipl.-Inf., Bernd Becker, Prof. Dr. Grouping Heuristics for Word-level Decision Diagrams IEEE International Symposium on Circuits and Systems, 1999 |
|
Wolfgang Günther, Dr., Rolf Drechsler, Prof. Dr., Stefan Höreth Efficient Dynamic Minimization of Word-Level DDs based on Lower Bound Computation Int'l Conf. on Comp. Design, 2000 |