Sciweavers

Share
FMCAD
2000
Springer

Scalable Distributed On-the-Fly Symbolic Model Checking

9 years 9 months ago
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...
Shoham Ben-David, Tamir Heyman, Orna Grumberg, Ass
Added 24 Aug 2010
Updated 24 Aug 2010
Type Conference
Year 2000
Where FMCAD
Authors Shoham Ben-David, Tamir Heyman, Orna Grumberg, Assaf Schuster
Comments (0)
books