This paper presents a method for specification as well as efficient formal verification of power gating feature of processors. Given an instruction-set architecture model of a processor, as the golden model, and a detailed processor model with power gating feature, we propose an efficient method for equivalence checking of the two models using symbolic simulation and property checking. Our experimental results on a MIPS processor shows that our method reduces the verification time compared to the correspondence checking method at least by 3.4x.