1. Scalable distributed on-the-fly symbolic model checking.
- Author
-
Ben-David, Shoham, Grumberg, Orna, Heyman, Tamir, and Schuster, Assaf
- Subjects
PARALLEL programming ,PARALLEL processing ,ELECTRONIC data processing ,COMPUTER algorithms ,COMPUTER systems ,COMPUTER science - Abstract
This paper presents a scalable method for parallel symbolic on-the-fly model checking in a distributed memory environment. Our method combines a scheme for on-the-fly model checking for safety properties with a scheme for scalable reachability analysis. We suggest an efficient, BDD-based algorithm for a distributed construction of a counterexample. The extra memory requirement for counterexample generation is evenly distributed among the processes by a memory balancing procedure. At no point during computation does the memory of a single process contain all the data. This enhances scalability. Collaboration between the parallel processes during counterexample generation reduces memory utilization for the backward step. We implemented our method on a standard, loosely-connected environment of workstations, using a high-performance model checker. Our initial performance evaluation, carried out on several large circuits, shows that our method can check models that are too large to fit in the memory of a single node. Our on-the-fly approach may find counterexamples even when the model is too large to fit in the memory of the parallel system. [ABSTRACT FROM AUTHOR]
- Published
- 2003
- Full Text
- View/download PDF