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:
- Boeing 747-400 Integrated Display System (IDS)
- Boeing 737-300 Electronic Flight Instrumentation System (EFIS)
- Boeing 777 Flight Control Backdrive
- Boeing 757,767 Autopilot Flight Director System (AFDS)
- 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.
-
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.
-
Srivas, Mandayam K.; and Miller, Steven P:
Formal Verification of an Avionics Microprocessor.
NASA Contractor Report 4682, August 1995.
-
Miller, Steve P:
The AAMP5/AAMP-FV Project,
Slides presented at the
Third NASA Langley Formal Methods Workshop,
May 10-12, 1995.
-
Srivas, Mandayam:
The Formal Verification Technology Used on AAMP5,
Slides presented at the
Third NASA Langley Formal Methods Workshop,
May 10-12, 1995.
-
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)
References
(These may be ordered)