Sequential equivalence checking is an important practical problem. Previously, sequential equivalence checking problems are either treated as general property checking problems or solved by finding an inductive set of internal equivalent signals. However, difficulties are encountered by either approach. In this thesis, we study several related techniques and derive a hybrid method that allows a property checking engine to utilize functionally equivalent signals to prove the equivalence of both circuits. Our method shows a bridge between very different approaches.