A Partitioning Methodology for BDD-Based Verification.
Subramanian K. Iyer,
David L. Dill and
E. Allen Emerson
The main challenge in BDD-based verification is dealing with the memory
explosion problem during reachability analysis.
In this paper we advocate a methodology to handle this problem based on
state space partitioning of functions as well as relations.
We investigate the key questions of how to perform partitioning in
reachability based verification and provide suitable algorithms.
We also address the problem of instability of BDD-based verification
by automatically picking the best configuration from different
short traces of the reachability computation.
Our approach drastically decreases verification time,
often by orders of magnitude.