Overlap reduction in symbolic system traversal

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.