Detecting hard faults with combined approximate forward / backwardsymbolic techniques

Symbolic state space exploration techniques proved to be useful not only in formal verification and synthesis, but also in testing. Most of them are based on exact forward or backward traversal. As an alternative, approximate forward traversal algorithms have been proposed, but they are not immediately applicable to test pattern generation. This paper presents strategies for approximate forward traversal, then it combines approximate forward traversal and backward traversal for generating test patterns for hard to detect faults. Efficient search space pruning is obtained by means of cofactoring. Experimental results show that the speed up ranges from 2 to more than 50.