DocumentCode :
1903074
Title :
Formal verification of a PowerPC microprocessor
Author :
Appenzeller, David P. ; Kuehlmann, Andreas
Author_Institution :
IBM Microelectron. Burlington, Essex Junction, VT, USA
fYear :
1995
fDate :
2-4 Oct 1995
Firstpage :
79
Lastpage :
84
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;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Computer Design: VLSI in Computers and Processors, 1995. ICCD '95. Proceedings., 1995 IEEE International Conference on
Conference_Location :
Austin, TX
ISSN :
1063-6404
Print_ISBN :
0-8186-7165-3
Type :
conf
DOI :
10.1109/ICCD.1995.528794
Filename :
528794
Link To Document :
بازگشت