FM Past Program: AAMP5/AAMP-FV Project

This page is not maintained. It is probably out of date.
A cooperative effort exists with Rockwell-Collins to apply formal methods to the design and verification of a formally-verified microprocessor, currently designated as AAMP-FV. This work builds on its successful predecessor project, the formal verification of parts of the design of the AAMP5, the latest member of the CAPS/AAMP family of microprocessors The CAPS/AAMP family of microprocessors has been widely used by the commercial and military aerospace industries. Some examples of use of earlier members of the family include:
  1. Boeing 747-400 Integrated Display System (IDS)
  2. Boeing 737-300 Electronic Flight Instrumentation System (EFIS)
  3. Boeing 777 Flight Control Backdrive
  4. Boeing 757,767 Autopilot Flight Director System (AFDS)
  5. military and commercial Global Positioning (GPS) Systems.
The goal of the AAMP5 project was to demonstrate the feasibility of applying formal methods to the design and verification of a widely used aerospace microprocessor.

Work began in Februrary, 1993 to formally specify the instruction set and the microarchitecture of the AAMP5 using SRI International's PVS (Prototype Verification System) tool. While formally specifying the microprocessor, two design errors were discovered in the microcode. These errors were uncovered as a result questions raised by the formal methods researchers at Collins and SRI International while seeking to formally specify the behavior of the microprocessor. The Collins formal methods team believes that this effort has prevented two significant errors from going into the first fabrication of the microprocessor.

References

  1. Srivas, Mandayam; and Miller, Steve P: Applying Formal Verification to a Commercial Microprocessor, in 1995 IFIP International Conference on Computer Hardware Description Languages, Chiba, Japan, August 1995. Chosen Best Paper of the Conference.

  2. Srivas, Mandayam K.; and Miller, Steven P: Formal Verification of an Avionics Microprocessor. NASA Contractor Report 4682, August 1995.

  3. Miller, Steve P: The AAMP5/AAMP-FV Project, Slides presented at the Third NASA Langley Formal Methods Workshop, May 10-12, 1995.

  4. Srivas, Mandayam: The Formal Verification Technology Used on AAMP5, Slides presented at the Third NASA Langley Formal Methods Workshop, May 10-12, 1995.

  5. Miller, Steven P; and Srivas, Mandayam: Formal Verification of the AAMP5 Microprocessor: A Case Study in the Industrial Use of Formal Methods, Presented at WIFT '95: Workshop on Industrial-Strength Formal Specification Techniques, April 5-8, 1995, Boca Raton, Florida USA, pp. 30-43.
Curator and Responsible NASA Official: C. Michael Holloway
last modified: 13 March 1996 (09:23:13)