Formal verification of the AAMP5 microprocessor: a case study in the industrial use of formal methods

Author

Miller, Steven P. ; Srivas, Mandayam

Author_Institution

Collins Commercial Avionics, Rockwell Int. Corp., Cedar Rapids, IA, USA

fYear

1995

fDate

5-8 Apr 1995

Firstpage

2

Lastpage

16

Abstract

This paper describes the experiences of Collins Commercial Avionics and SRI International informally specifying and verifying the microcode for the AAMP5 microprocessor with the PVS verification system. This project was conducted to determine if an industrial microprocessor designed for use in real-time embedded systems could be formally specified at the instruction set and register transfer levels and if formal proofs could be used to prove the microcode correct. The paper provides a brief technical overview, but its emphasis is on the lessons learned in using PVS for an example of this size and the implications for using formal methods in an industrial setting

Keywords

computer testing; firmware; formal verification; integrated circuit testing; microprocessor chips; real-time systems; AAMP5 microprocessor; PVS verification system; formal methods; formal proofs; formal verification; industrial microprocessor; instruction set level; microcode; real-time embedded systems; register transfer level; Aerospace electronics; Computer aided software engineering; Computer science; Error correction; Formal specifications; Formal verification; Hardware; Laboratories; Microprocessors; NASA;

fLanguage

English

Publisher

ieee

Conference_Titel

Industrial-Strength Formal Specification Techniques, 1995. Proceedings., Workshop on

Conference_Location

Boca Raton, FL

Print_ISBN

0-8186-7005-3

Type

conf

DOI

10.1109/WIFT.1995.515475

Filename

515475