A New Method for Verifying Sequential Circuits

We present an algorithm for deciding whether two given synchronous, logic-level sequential circuits are functionally equivalent. Our approach involves a formal symbolic comparison, as opposed to the (often very time-consuming) generation and simulation of numerous test vector sequences. The given circuits need not have the same number of states, nor must they have the same number of inputs -- for example, one circuit may be a parallel implementation and the other serial. Although this is an intractable problem in general, we believe that the method is useful on a broad class of practical circuits; our computational experience thus far is encouraging.