Home Intro Wiki Docs FAQ Download Bugs Mail FM Tools

Applying Formal Verification to a Commercial Microprocessor

Mandayam Srivas (SRI) and Steven P. Miller (Collins Commercial Avionics)

From the proceedings of the 1995 IFIP International Conference on Computer Hardware Description Languages, Chiba, Japan, August 1995, pp. 493-502. This was judged "Best paper" by the CHDL Program Committee.

Abstract

Formal verification using interactive proof-checkers has been used successfully to verify a wide variety of moderate-sized hardware designs. The industry is beginning to look at formal verification as an alternative to simulation for obtaining higher assurance than is currently possible. However, many questions remain regarding its 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 describes a project recently undertaken by SRI International and Collins Commercial Avionics, a division of Rockwell International to explore some of these questions. The project formally specified in SRI's PVS language a Rockwell proprietary pipelined microprocessor (the AAMP5, built using almost half a million transistors) at both the instruction-set and register-transfer levels and used the PVS theorem prover to show the microcode correctly implemented the instruction-level specification for a representative subset of instructions. The key results of the project were the development of a practical methodology for microprocessor verification in industrial settings and the discovery of both actual and seeded errors.

postscript only

BibTeX Entry

@inproceedings{Srivas&Miller95:chdl,
	TITLE = {Applying Formal Verification to a Commercial Microprocessor},
	AUTHOR = {Mandayam K. Srivas and Steven P. Miller},
	PAGES = {493--502},
	BOOKTITLE = {{CHDL '95}: 12th Conference on Computer Hardware
		Description Languages and their Applications},
	EDITOR = {Steven D. Johnson},
	ORGANIZATION = {Proceedings published in a single volume jointly
		with ASP-DAC '95, CHDL '95, and VLSI '95, IEEE Catalog
		no.\ 95TH8102},
	MONTH = aug,
	YEAR = 1995,
	ADDRESS = {Chiba, Japan}
}
Home Intro Wiki Docs FAQ Download Bugs Mail FM Tools

Last modified: Thu 30 Nov 2006 12:15 UTC
Maintainer: Sam Owre