Scalable Distributed On-the-Fly Symbolic Model Checking

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...

• Type: Conference
• Year: 2000
• Where: FMCAD
• Authors: Shoham Ben-David, Tamir Heyman, Orna Grumberg, Assaf Schuster
• Keywords: Distributed Memory Environment, FMCAD 2000, Formal Methods, On-the-fly Model Checking, Symbolic On-the-fly Model