Paper Info
Title
Applying formal verification to the AAMP5 microprocessor: a case study in the industrial use of formal methods
Abstract
Formal specification combined with mechanical verification is a promising approach for achieving the extremely high levels of assurance required of safety-critical digital systems. However, many questions remain regarding their use in practice: Can these techniques scale up to industrial systems, where are they likely to be useful, and how should industry go about incorporating them into practice? This paper discusses a project undertaken to answer some of these questions, the formal verification of the microcode in the AAMP5 microprocessor. This project consisted of formally specifying in the PVS language a Rockwell proprietary microprocessor at both the instruction-set and register-transfer levels and using the PVS theorem prover to show the microcode correctly implemented the instruction-level specification for a representative subset of instructions. Notable aspects of this project include the use of a formal specification language by practicing hardware and software engineers, the integration of traditional inspections with formal specifications, and the use of a mechanical theorem prover to verify a portion of a commercial, pipelined microprocessor that was not explicitly designed for formal verification.
Year
DOI
Venue
1996
10.1007/BF00122419
Formal Methods in System Design
Keywords
Field
DocType
safety critical systems,formal method,industrial use,pvs,hardware verification systems,formal methods,microcode verification,aamp5 microprocessor,microprocessor verification,case study,formal verification,theorem prover,register transfer level,formal specification,software engineering,system safety
Microcode,Programming language,Life-critical system,Computer science,Microprocessor,Automated theorem proving,Formal specification,Theoretical computer science,Software,Formal methods,Formal verification
Journal
Volume
Issue
ISSN
8
2
0925-9856
Citations 
PageRank 
References 
35
4.80
12
Authors
2
Name
Order
Citations
PageRank
Mandayam K. Srivas147164.76
Steven P. Miller256156.48