Invariant Checking Combining Forward and Backward Traversal

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