One of the big challenges in circuit design is the formal verification at clocked algorithmic or register-transfer level. To overcome the limits of BDD based approaches we apply an abstraction of the datapath by uninterrupted functions [2]. A function f is uninterrupted if all properties except \math are dropped.In the past symbolic execution and theorem proving were used to check the equivalence of two sequential circuits that Are abstracted by uninterrupted functions. Symbolic execution is an enumeration of states reachable from the initial state [2]. Because of the uninterrupted functions there is no general termination condition of such procedures. In the theorem prover based approach [4] the proof is usually carried out using the induction principle. Often lemmas are needed to prove the equivalence. These lemmas are also proven by induction. These lemmas are often in-variants.The proof of the induction step is automated by decision procedures. In our approach symbolic execution is used to generate potential invariants. Then the equivalence is proven by automatic induction proofs of the lemmas. A more detailed description of the procedure can be found in [3].