A scalable parallel algorithm for reachability analysis of very large circuits

Abstract

This paper presents a scalable method for parallelizing symbolic reachability analysis on a distributed-memory environment of workstations. We have developed an adaptive partitioning algorithm that significantly reduces space requirements. The memory balance is maintained by dynamically repartitioning the state space throughout the computation. A compact BDD representation allows coordination by shipping BDDs from one machine to another. This representation allows for different variable orders in the sending and receiving processes. The algorithm uses a distributed termination protocol, with none of the memory modules preserving a complete image of the set of reachable states. No external storage is used on the disk. Rather, we make use of the network, which is much faster. We implemented our method on a standard, loosely-connected environment of workstations, using a high-performance model checker. Initial performance evaluation of several large circuits shows that our method can handle models too large to fit in the memory of a single node. The partitioning algorithm achieves reduction in space, which is linear in the number of workstations employed. A corresponding decrease in space requirements is measured throughout the teachability analysis. Our results show that the relatively slow network does not become a bottleneck, and that computation time is kept reasonably small.