Sequential Equivalence Checking Algorithm Using States Caching

An improved algorithm based on register mapping is proposed to increase the speed of equivalence checking for sequential circuits. It not only used pre-image computation to avoid false negative, but also incorporated reachable states and unreachable states in the verification process. States that can be reached from the initial state in simulation are collected as reachable states, states that cannot be reached from the initial state in verification are collected as unreachable states,they are used to reduce pre-image computation. Experimental results based on mcnc91 show that the algorithm can reduce verification time efficiently.