Title :
Formal verification of a PowerPC microprocessor
Author :
Appenzeller, David P. ; Kuehlmann, Andreas
Author_Institution :
IBM Microelectron. Burlington, Essex Junction, VT, USA
Abstract :
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
Keywords :
formal verification; logic design; logic testing; microprocessor chips; BDD-based verification tool; PowerPC microprocessor; formal methods; register-transfer level specification; transistor level implementation; verification; Boolean functions; CMOS logic circuits; Circuit synthesis; Circuit testing; Data structures; Formal verification; Logic design; Microprocessors; Registers; Switches;
Conference_Titel :
Computer Design: VLSI in Computers and Processors, 1995. ICCD '95. Proceedings., 1995 IEEE International Conference on
Conference_Location :
Austin, TX
Print_ISBN :
0-8186-7165-3
DOI :
10.1109/ICCD.1995.528794