Formale Verifikation mit Decision Diagrams
| project staff | project description | publications
|
| former employee Chair of Computer Architecture | |
| Wolfgang Günther, Dr. | |
| Rolf Drechsler, Prof. Dr. | |
| Marc Herbstritt, Dr. | |
Formal verification deals with proving the correctness of a given design. Thereby the specification can be given in different levels of abstraction. In many cases BDDs are used as the basic data structure for verification. Under all variable orderings however, BDDs have exponential size for multipliers. In order to avoid this problem Word Level Decision Diagrams like BMDs oder K*BMDs are often used. The lower bounds which are used for BDDs could be adapted for K*BMDs.
|
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 |