Name
Abstract | ||
|---|---|---|
Not long ago, completely automatical formal verification of multipliers was not feasible, even for small input word sizes. However, with Multiplicative Binary Moment Diagrams (*BMD), which is a new data structure for representing arithmetic functions over Boolean variables, methods were proposed by which verification of multipliers with input word sizes of up to 256 Bits is now feasible. Unfortunately, only experimental data has been provided for these verification methods until now.In this paper, we give a formal proof that logic verification with *BMDs is polynomially bounded in both, space and time, when applied to the class of Wallace-tree like multipliers. Using this knowledge online detection of design errors becomes feasible during a verification run. |
Year | DOI | Venue |
|---|---|---|
2003 | 10.1023/A:1021752130394 | formal methods |
Keywords | DocType | Volume |
equivalence checking,formal verification,integer multipliers,backward construction,multiplicative binary moment diagrams | Journal | 22 |
Issue | ISSN | Citations |
1 | 1572-8102 | 16 |
PageRank | References | Authors |
0.92 | 15 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Martin Keim | 1 | 26 | 1.53 |
| Rolf Drechsler | 2 | 3707 | 351.36 |
| Bernd Becker | 3 | 855 | 73.74 |
| Michael Martin | 4 | 16 | 0.92 |
| P. Molitor | 5 | 211 | 18.50 |