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.
