Efficient state space pruning in symbolic backward traversal

Most symbolic state space exploration techniques for finite state machines (FSMs) are exact and based on forward traversal, but limited to medium-size circuits. Approximate forward traversal deals with bigger circuits at the expense of exactness. Backward traversal focuses the search process on the property under scrutiny, but it also takes into account many unreachable states. For this reason, it works mainly on small circuits. This paper presents novel techniques that make exact symbolic backward traversal feasible also for large circuits. The key point is an efficient pruning of the search space, exploiting information coming from an approximate forward reachability analysis. Experimental evidence shows that, for the first time, the larger ISCAS´89 and MCNC circuits are symbolically manipulated in an exact way and the test patterns for them are generated