EXACT CALCULATION OF SYNCHRONIZING SEQUENCES BASED ON BINARY DECISIONDIAGRAMS

In order to reliably predict the behavior of a finite state machine (F SM) M or to generate acceptance tests for sequential designs, it is ne cessary to drive M to a predictable state or set of states. One possib le way to accomplish this is to have a special reset circuit to force all the latches to a specific state. However, if the circuit can be dr iven to a predictable state by applying an input sequence, the area re quired for reset circuitry can be saved. A synchronizing sequence for an FSM M is an input sequence which, when applied to any initial state of M, will drive M to a single specific state, called a reset state. An efficient and exact method for computing synchronizing sequences ba sed on the efficient image and pre-image computation methods using bin ary decision diagrams is presented. The method is exact in the sense t hat it is a decision procedure: Given enough time and memory, the meth od can compute a synchronizing sequence if has one; otherwise, the met hod says that M is not resettable. The theoretical heart of the propos ed method is Universal Alignment, which is an analysis of the product of an FSM with itself. Algorithms and their related theorems are prese nted to perform the following: decide whether M has a synchronizing se quence (i.e., M is resettable). calculate a synchronizing sequence for M. calculate the set of all reset states. decide whether a specific s tate is a reset state. New results on the resettability of some benchm ark circuits are reported.