Exact calculation of synchronizing sequences based on binary decision diagrams

In order to reliably predict the behavior of a finite state machine (FSM) M or to generate acceptance tests for sequential designs, it is necessary to drive M to a predictable state or set of states. One possible way of accomplishing this is to have a special reset circuit to force all the latches to a specific state. However, if the circuit can be driven to a predictable state by applying an input sequence, the area required 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 based on the efficient image and pre-image computation methods using binary decision diagrams is presented. The method is exact in the sense that it is a decision procedure: Given enough time and memory, the method can compute a synchronizing sequence if M has one; otherwise, the method says that M is not resettable. The theoretical heart of the proposed method is Universal Alignment, which is an analysis of the product of an FSM with itself. Algorithms and their related theorems are presented to perform the following: decide whether M has a synchronizing sequence (i.e., M is resettable), calculate a synchronizing sequence for M, calculate the set of all reset states, decide whether a specific state is a reset state. New results on the resettability of some benchmark circuits are reported