A New Reachability Algorithm for Symmetric Multi-processor Architecture

Partitioned BDD-based algorithms have been proposed in the literature to solve the memory explosion problem in BDD-based verification. A naive parallelization of such algorithms is often ineffective as they have less parallelism. In this paper we present a novel parallel reachability approach that lead to a significantly faster verification on a Symmetric Multi-Processing architecture over the existing onethread, one-CPU approaches. We identify the issues and bottlenecks in parallelizing BDD-based reachability algorithm. We show that in most cases our algorithm achieves good speedup compared to the existing sequential approaches. Key words: Reachability, Algorithm, Parallel, Multi-threaded

• Type: Conference
• Year: 2005
• Where: ATVA
• Authors: Debashis Sahoo, Jawahar Jain, Subramanian K. Iyer, David L. Dill
• Keywords: ATVA 2005, BDD-based Reachability Algorithm, Memory Explosion Problem, Symmetric Multi-Processing Architecture