Name
Abstract | ||
|---|---|---|
A divide-and-conquer approach in BDD-based verification to handle larger designs is to partition BDDs exceeding a threshold size and to deal with the partitions separately. Crossover transitions to the same state cause the main problem of this methodology, because they result in overlap of the partitions and thus introduce redundant computations when dealing with the partitions. In this paper we describe an algorithm for splitting Boolean functions representing state sets of synchronous systems such that in subsequent symbolic traversal of the resulting subsets the state set overlap is reduced. We demonstrate the effectiveness of our splitting algorithm by applying it in sequential and distributed versions of a bounded property checking algorithm. Also, a dynamic extension to static overlap reduction is sketched. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1109/HLDVT.2005.1568829 | HLDVT |
Keywords | Field | DocType |
divide-and-conquer approach,bounded property checking algorithm,state set,crossover transition,splitting boolean function,main problem,symbolic system traversal,splitting algorithm,bdd-based verification,larger design,dynamic extension,boolean function,boolean functions,divide and conquer | Boolean function,Dynamic Extension,Crossover,Model checking,Tree traversal,Computer science,Algorithm,Theoretical computer science,Symbolic system,Boolean expression,Bounded function | Conference |
ISSN | ISBN | Citations |
1552-6674 | 0-7803-9571-9 | 1 |
PageRank | References | Authors |
0.35 | 24 | 6 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| P. M. Peranandam | 1 | 4 | 0.72 |
| P. K. Nalla | 2 | 1 | 0.35 |
| R. J. Weiss | 3 | 4 | 0.72 |
| Jürgen Ruf | 4 | 122 | 23.04 |
| T. Kropf | 5 | 4 | 1.06 |
| W. Rosenstiel | 6 | 15 | 4.15 |