Invariant checking combining forward and backward traversal

Abstract

In invariant checking two directions of state space traversal are possible: Forward from initial states or backward starting from potential error states. It is not clear in advance, which direction will be computationally easier or will terminate in fewer steps. This paper presents a dynamic approach based on OBDDs for interleaving forward and backward traversal. The approach increases the chance for selecting the shorter direction and at the same time limits the overhead due to redundant computation. Additionally, a second approach using two OBDDs with different variable orders is presented, providing improved completion at the cost of some additional overhead. These approaches result in a dramatic gain in efficiency over unidirectional traversal. For the first time all benchmarks of the VIS-Verilog suite have been finished using a BDD-based method. © Springer-Verlag 2004.