Abstract: With the increasing complexity of integrated circuits designs, functional verification has become the bottle-neck of design flow. The traditional simulation based validation is very time-consuming and incomplete. An alternative technique is formal verification, it needs no test vector, and can reduce the design cycle with full functional coverage. In this paper, we present an equivalence checking scheme for verifying a general purpose CPU design, including proving the equivalence of two designs in different levels of abstraction (e.g. RTL to gates, gates to gates, RTL to RTL). The techniques to solve some common problems are proposed. The verification results show that the proposed scheme can reduce the gate-level simulation time significantly, and increase confidence in the system design.