Symbolic forward/backward traversals of large finite state machines

Symbolic traversals are state-of-the-art techniques for proving the input/o utput equivalence of finite state machines. Due to state space explosion, t hey are currently limited to medium-small circuits. Starting from the limit s of standard techniques, this paper presents a mix of approximate forward and exact backward traversals that results in an exact exploration of the s tate space of large machines. This is possible, thanks to efficient pruning that restricts the search space during backward traversal using the inform ation coming from the approximate forward traversal step. Experimental resu lts confirm that we are able to explore for the first time some of the larg er ISCAS'89 and MCNC circuits, that have been until now outside the scope o f exact symbolic techniques. We are also able to generate the test patterns for or to tag as undetectable stuck-at faults with few exceptions. (C) 200 0 Elsevier Science B.V. All rights reserved.