Application name:

AAMP-FV

Organisation:

* Collins Avionics & Communications * SRI

Method:

PVS

Tools:

PVS

Domain:

Microcode Verification, Hardware Modeling.

Period:

October 1994 -- August 1996

Size:

Specification of the macroarchitecture (3,693 lines of PVS) + Specification of the microarchitecture (3,496 lines of PVS) AAMP-FV Microprocessor Design - Approximately 100,000 transistors.

Description:

This project consisted of specifying in the PVS language a portion of the design for 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. This project was conducted to determine if the expertise gained during the AAMP5 project could be used to bring the cost of formal verification down to an acceptable level.

Conclusions:

The key result of the AAMP-FV project was to confirm that the expertise gained on the AAMP5 project could be exploited to reduce the cost of formal verification dramatically. Of the 80 AAMP-FV instructions, 54 were proven correct. More importantly, the cost of their verification dropped by almost an order of magnitude from that observed on the AAMP5 project. However, as more complex instructions were attempted, proof techniques first developed on the AAMP5 project broke down and new approaches had to be devised. This phase progressed more as an exploratory project, with a steep learning curve and unexpected delays. One of the main contributions of the AAMP-FV project was the development of methods to handle instructions with complex microcode.

Publications:

"Formal Verification of the AAMP5 and AAMP-FV Microcode". Steven P. Miller, David A. Greve, and Mandayam K. Srivas, in Proceedings of the Third AMAST Workshop on Real-Time Systems, Salt Lake City, Utah, March 6-8, 1996.

Contact:

Name:	Steven P. Miller
Organisation:	Collins Avionics & Communications
Address:	Rockwell Collins, Inc. Cedar Rapids, IA 52498
Country:	USA
E-mail:	spmiller@collins.rockwell.com
Personal website:	none

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:	none

URL:

none

Remarks:

none

© copyright 2004 | Formal Methods Europe