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 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. Categories and Subject Descriptors B.6.3 [Logic Design]: Design Aids--Verification General Terms Algorithms, Measurement, Verification Keywords Reachability Analysis, Parallel, Multi-threaded

• Type: Conference
• Year: 2005
• Where: DAC
• Authors: Debashis Sahoo, Jawahar Jain, Subramanian K. Iyer, David L. Dill, E. Allen Emerson
• Keywords: DAC 2005, Design Automation, Multi-threaded Reachability Algorithm, Standard Reachability Algorithm, Verification Keywords Reachability