Applying formal verification to the AAMP5 microprocessor: A case study in the industrial use of formal methods

作     者：Srivas, MK Miller, SP 

作者机构：SRI INTCOMP SCI LABMENLO PKCA 94025 ROCKWELL INT CORPCOLLINS COMMERCIAL AVIONCEDAR RAPIDSIA 52498 

出 版 物：《FORMAL METHODS IN SYSTEM DESIGN》 (系统设计中的形式方法)

年 卷 期：1996年第8卷第2期

页      面：153-188页

核心收录：

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主　　题：formal methods formal verification microprocessor verification microcode verification hardware verification systems safety critical systems PVS 

摘      要：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 paper discusses a project undertaken to answer some of these questions, the formal verification of the microcode in the AAMP5 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 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.