Efficient decision ordering techniques for SAT-based test generation

Model checking techniques are promising for automated generation of directed tests. However, due to the prohibitively large time and resource requirements, conventional model checking techniques do not scale well when checking complex designs. In SAT-based BMC, many variable ordering heuristics have been investigated to improve counterexample (test) generation involving only one property. This paper presents efficient decision ordering techniques that can improve the overall test generation time of a cluster of similar properties. Our method exploits the assignments of previously generated tests and incorporates it in the decision ordering heuristic for current test generation. Our experimental results using both software and hardware benchmarks demonstrate that our approach can drastically reduce the overall test generation time.