Symbolic forward/backward traversals of large finite state machines

Symbolic traversals are state-of-the-art techniques for proving the input/output equivalence of finite state machines. Due to state space explosion, they are currently limited to medium-small circuits. Starting from the limits of standard techniques, this paper presents a mix of approximate forward and exact backward traversals that results in an exact exploration of the state space of large machines. This is possible, thanks to efficient pruning that restricts the search space during backward traversal using the information coming from the approximate forward traversal step. Experimental results confirm that we are able to explore for the first time some of the larger ISCASʹ89 and MCNC circuits, that have been until now outside the scope of exact symbolic techniques. We are also able to generate the test patterns for or to tag as undetectable stuck-at faults with few exceptions.