Formal verification of a PowerPC microprocessor

This paper presents the use of formal methods in the design of a PowerPC microprocessor. The chosen methodology employs two independently developed design views, a register-transfer level specification for efficient system simulation and a transistor level implementation geared toward maximal processor performance. A BDD-based verification tool is used to functionally compare the two views which essentially validates the transistor-level implementation with respect to any functional simulation/verification performed at the register-transfer level. We show that a tight integration of the verification approach into the overall design methodology allows the formal verification of complex microprocessor implementations without compromising the design process or performance of the resulting system