Application name:

AAMP5

Organisation:

Collins Avionics and Communications; SRI

Method:

PVS

Tools:

PVS

Domain:

Microcode Verification, Hardware Modeling

Period:

January 1993 - August 1994

Size:

Specification of the macroarchitecture (2550 lines of PVS) + Specification of the microarchitecture (2679 lines of PVS) AAMP5 Microprocessor - Approximately 500,000 transistors

Description:

This project consisted of specifying in the PVS language a portion of 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 specified behavior for a representative subset of instructions.

Conclusions:

The central result of this project was to demonstrate the technical feasibility of formally specifying a commercial microprocessor and the use of mechanical proofs of correctness to verify microcode. This is particularly significant since the AAMP5 was not designed for formal verification, but to provide a more than three fold performance improvement over the earlier AAMP2. Two actual microcode errors were discovered and corrected during development of the formal specification, and two seeded errors were discovered while doing correctness proofs. Eleven instructions, representative of several classes of instructions, were actually verified. Much of the time spent on the proofs was invested in the development of reusable proof strategies. It was also demonstrated that practicing engineers could read and conduct inspections of formal specifications written in PVS. While the cost of the formal verification was high, much of this can be attributed to the exploratory nature of the work. Formal verification did provide a very high level of assurance. To provide the same level of assurance, traditional methods would be just as, if not more, expensive than formal methods.

Publications:

"Formal Verification of the AAMP5 Microcode: A Case Study in the Industrial Use of Formal Methods". Mandayam K. Srivas (SRI) and Steven P. Miller (Collins Commercial Avionics), Formal Methods in System Design Vol 8, No 2, pages 153-188, March 1996

"Formal Verification of an Avionics Microprocessor". Mandayam K. Srivas (SRI) and Steven P. Miller (Collins Commercial Avionics). NASA Contractor Report 4682, NASA Langley Research Center, Hampton, Virginia, July 1995. Also available as SRI Technical Report SRI-CSL-95-4.

"Applying Formal Verification to a Commercial Microprocessor". Mandayam Srivas (SRI) and Steven P. Miller (Collins Commercial Avionics). Presented at the 1995 IFIP International Conference on Computer Hardware Description Languages, Chiba, Japan, August 1995.

"Formal Verification of the AAMP5 Microprocessor--A Case Study in the Industrial Use of Formal Methods". Steven P. Miller and M. Srivas, presented at the Workshop on Industrial-Strength Formal Specification Techniques (WIFT'95), Boca Raton, Florida, April, 1995.

"Formal Verification of the AAMP5 Microprocessor". Steven P. Miller and M. Srivas, Applications of Formal Methods, M. G. Hinchey and J.P. Bowen (eds), Prentice Hall International, 1995, pp 125--180, 1995.

Contact:

Name:	Mandayam Srivas
Organisation:	Computer Science Laboratory, SRI International
Address:	Menlo Park, CA 94025
Country:	USA
E-mail:	Srivas@csl.sri.com
Personal website:	-

URL:

-

Remarks:

-

© copyright 2004 | Formal Methods Europe