1. Field of the Invention
The present invention relates generally to a method for using Complete-1-Distinguishability for FSM equivalence checking. More particularly, the subject invention pertains to a methodology that simplifies the problem of FSM verification, and considers the case where the specification FSM has a Complete-1-Distinguishability (C-1-D) property, i.e. all state pairs are 1-distinguishable. The main idea is that if each state of the specification FSM can be distinguished from all others by an input sequence of length 1, then the only equivalence class of the implementation FSM which is possibly equivalent to it, can be easily found by using a mapping induced by 1-equivalence between the states of the two FSMs.
2. Discussion of the Prior Art
Checking the equivalence of finite state machines (FSMs) is an important problem in formal verification of hardware designs. The basic algorithm for checking the equivalence of two FSMs consists of first building a product state machine by a parallel composition of the individual machines. This product state machine has lockstep transitions on the common inputs, and it is checked that the outputs of the two machines are identical in every state pair which is reachable from the initial state pair. The reachability of the product state pair is an essential requirement in this check. Therefore, in the general case, a traversal needs to be performed on the product state space. Typically, this traversal is done symbolically by using Binary Decision Diagrams (BDDs) to represent the state transition functions (or relations) and the sets of reachable states. Research in this direction has led to numerous techniques that focus on forward traversal, backward traversal, as well as approximate traversal. As with most BDD-based techniques, their practical limitations stem from extensive memory requirements, especially when handling large machines.
Though the general FSM equivalence problem requires state space traversal of the product machine, simplifications are possible by placing restrictions on the synthesis process. In particular, if the latch boundaries in the pre-synthesis specification are fixed and maintained throughout synthesis, then the resulting implementation has the same state encoding with a known correspondence of latches. In this case, it suffices to perform a combinational equivalence check on the output and next-state functions of the two machines. (The combinational checks can be restricted to reachable states in order to give an exact result.) Numerous researchers, as well as some commercial tools, have used this combinational methodology to check sequential circuits in practice.