Sequential equivalence checking based on structural similarities

Checking the functional equivalence of sequential circuits is an important practical problem. Because general algorithms for solving this problem require a state-space traversal of the product machine, they are computationally expensive. In this paper, we present a new method for sequential equivalence checking which utilizes functionally equivalent signals to prove the equivalence of both circuits, thereby avoiding the state-space traversal. The effectiveness of the proposed method is confirmed by experimental results on retimed and optimized ISCAS'89 benchmarks