SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
     
  SRI Logo

Formal Verification of an Avionics Microprocessor
 by Mandayam K. Srivas & Steve P. Miller.

Abstract
Formal specification combined with mechanical verification is a promising approach for achieving the extremely high levels of assurance required of safety-critical digital systems. However. many questions remain regarding their 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 report discusses a project undertaken to answer some of these questions, the formal verification of the AA11PS microprocessor. This project consisted of formally specifying in the PVS language a Rockwell proprietary microprocessor at both the instruction set and register-transfer levels and using the PVS theorem prover to show that the microcode correctly implemented the instruction-level specification for a representative subset of instructions, Notable aspects of this project include the use of a formal specification language by practicing hardware and software engineers. the integration of traditional inspections with formal specifications. and the use of a mechanical theorem prover to verify a portion of a commercial, pipelined microprocessor that was not explicitly designed for formal verification,
Files
 













 

About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2017 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy