High-level formal verification of next-generation microprocessors

Author

Schubert, Tom

Author_Institution

DPG CPU Design Validation, Intel Corp., Hillsboro, OR, USA

fYear

2003

fDate

2-6 June 2003

Firstpage

1

Lastpage

6

Abstract

Formal property verification has been an effective complement to pre-silicon validation of several Intel® Pentium® 4 CPU designs at Intel Corporation. The principal objective of this program has been to prove design correctness rather than hunt for bugs. In the process, we have evolved our tools and methodology and are now applying FPV techniques to protocol level properties. Moving forward, new technologies such as GSTE and SAT offer the potential to significantly increase the scope of what can be formally verified. This paper discusses the application of FPV to validation of the Intel® Pentium® 4 microarchitecture and some approaches being considered to broaden the application of FV techniques, particularly at a higher level of design abstraction.

Keywords

formal verification; high level synthesis; microprocessor chips; CPU design; FPV technique; GSTE; Intel®Pentium® 4; SAT; design abstraction; formal property verification; high-level formal verification; next-generation microprocessor; pre-silicon validation; protocol level properties; Arithmetic; Computer bugs; Formal verification; Logic design; Microarchitecture; Microprocessors; Permission; Process design; Protocols; Silicon;

fLanguage

English

Publisher

ieee

Conference_Titel

Design Automation Conference, 2003. Proceedings

Print_ISBN

1-58113-688-9

Type

conf

DOI

10.1109/DAC.2003.1218767

Filename

1218767