This chapter introduces a processor verification methodology named EPEX which is based on a new form of equivalence checking. The core idea of this methodology is that two equivalent but distinct programs must produce the same result. By using a formal model of the processor specification, a test program can be transformed into an equivalent program. This “broadening” of the test program will activate different control and data paths in the hardware thus improving the chance for uncovering bugs. We evaluated EPEX on several experiments, including mutation experiments and the measurement of the control path variation produced by EPEX.