Division

Division Overview
Distributed Symbolic Model Checking Research Platform

In recent years, symbolic model checking became popular for formal verification of hardware designs. However, the applicability of this technique to ever larger designs is restricted because of extreme requirements for computing resources in terms of memory and CPU cycles.

Our research employs distributed computation to deal with the memory requirements of model checking. The goal is to solve problems that cannot fit into the memory of a single machine. This is accomplished by using large clusters of nodes, each contributing memory and CPU power, to build a machine that is large enough to handle the problem.

The initial results of this research have been published in leading journals and conferences and have thus caught the attention of both the academic world and industry. First we used IBM's model checker RuleBase (built on top of the SMV) for our performance results. During the past year we have developed the Division system, which is intended to be an open source system for researching distributed symbolic model checking on machines with hundreds of nodes.

This is pilot research. Real results can be obtained only by measuring runtime data. How a large number of nodes affects communication is also difficult to measure by simulation. In the following weeks, we hope to extend the size of the problems we can deal with by using the Division system on as many nodes as possible.