Uni-Logo
English       Login
Rechnerarchitektur
        Startseite         |         Institut für Informatik         |         Technische Fakultät
 

Formale Verifikation mit Decision Diagrams

| Beteiligte Mitarbeiter | Projektbeschreibung | Publikationen |


Beteiligte Mitarbeiter

ehemaliger Mitarbeiter Lehrstuhl ür Rechnerarchitektur
Marc Herbstritt, Dr.
Rolf Drechsler, Prof. Dr.
Wolfgang Günther, Dr.


Projektbeschreibung

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.



Publikationen
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