Verification of interacting sequential circuits

The problem of verifying the equivalence of interacting finite state machines (FSMs) described at the logic level is addressed. The problem is formulated as that of checking for the equivalence of the reset/starting states of the two FSMs. Separate sum-of-product representations of the on-sets and off-sets of each of the flip-flop inputs and primary outputs of the sequential circuit are extracted using the PODEM algorithm. A fast algorithm for state differentiation based on this representation is described. The input and the state space are implicitly enumerated through a process of repeated cube intersections to generate the state transition graph. Unlike previous approaches, this algorithm can be efficiently generalized for verifying distributed-style specifications of interacting sequential circuits, exploiting the nature of the interconnection topology. Pipeline latches in a distributed-style specification typically do not add complexity to the sequential behavior of a circuit, but greatly add to the complexity of traditional approaches to verifying sequential circuits. Pipeline latches are easily incorporated into this generalized, hierarchical verification strategy whereby the states of pipeline latches can be implicitly enumerated