Multi-threaded Reachability
Debashis Sahoo,
Jawahar Jain,
Subramanian K. Iyer,
David L. Dill and
E. Allen Emerson
DAC'05
Partitioned BDD-based algorithms have been proposed in the literature
to solve the memory explosion problem in BDD-based verification.
Such algorithms can be at times ineffective as they suffer from the
problem of scheduling the relative order in which the partitions
are processed. In this paper we present a novel multi-threaded
reachability algorithm that avoids this scheduling problem while
increasing the latent parallelism in partitioned state space
traversal. We show that in most cases our method is significantly
faster than both the standard reachability algorithm as well as the
existing partitioned approaches. The gains are further magnified
when our threaded implementation is evaluated in the context of a
parallel framework.