Minimum Length Synchronizing Sequences of Finite State Machine

Computing synchronizing sequences is an important step in test generation for circuits without external reset [CJSP93]. An efficient heuristic algorithm has been recently proposed [PJH92]. However, the only algorithms known so far for the minimum-length synchronizing sequence have been applicable only to small finite state machines, because they required excessive enumeration. In this paper we present a new technique to calculate the minimum length synchronizing sequence of a finite state machine, based on the BDD model of an iterative system. It implicitly calculates all possible minimum length sequences and corresponding reset states by deciding the satisfiability of a boolean formula. We also present a procedure to obtain the synchronizing sequences of a class of sequential iterative systems in constant time regardless of the number of cells. We present experimental results that show the viability of the proposed method for much larger circuits than were tractable by previous exact methods.