Scalable distributed on-the-fly symbolic model checking

Shoham Ben-David, Tamir Heyman, Orna Grumberg, Assaf Schuster

To appear at Formal Methods in Computer Aided Design (FMCAD00), Austin, Texas, November 1-3, 2000


This paper presents a scalable method for parallel symbolic on-the-fly model checking on a distributed-memory environment of workstations. Our method combines a parallel version of the model checking for RCTL safety properties with a scalable scheme for reachability analysis. The extra load of storage required for counter example generation is evenly distributed among the processes by our memory balancing. For the sake of scalability, at no point during the computation the memory of a single process contains all the data from any of the cycles. The counter example generation is thus performed through collaboration of the parallel processes. We develop a method for the counter example generation keeping a low peak memory requirement during the backward step and the computation of the inverse transition relation. We implemented our method on a standard, loosely-connected environment of workstations, using a high-performance SMV-based model checker. Our initial performance evaluation using 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 counter examples even when the model is too large to fit in the memory of the parallel system.

Server START Conference Manager
Update Time 26 Jun 2000 at 16:35:39
Start Conference Manager
Conference Systems