Multi-threaded reachability

Partitioned BDD-based algorithms have been proposed in the literature to solve the memory explosion problem in BDD-based verification. Such algorithms could be at times ineffective as they suffer from the problem of scheduling the relative order in which the partitions are processed. In this paper the authors presented a novel multi-threaded reachability algorithm that avoids this scheduling problem while increasing the latent parallelism in partitioned state space traversal. It is shown that in most cases this method is significantly faster than both the standard reachability algorithm as well as the existing partitioned approaches. The gains are further magnified when the threaded implementation is evaluated in the context of a parallel framework.