Formal Verification of the Aamp5 Microprocessor 1 2.1 Aamp Family of Microprocessors 2.2 Pvs 2.3 Historical Perspective/scale of the Challenge 2.4 Overview of the Technical Approach
Formal Verification of the Aamp5 Microprocessor 1 2.1 Aamp Family of Microprocessors 2.2 Pvs 2.3 Historical Perspective/scale of the Challenge 2.4 Overview of the Technical Approach
复制标题
Aamp5 微处理器的形式验证 1 2.1 Aamp 系列微处理器 2.2 Pvs 2.3 挑战的历史视角/规模 2.4 技术方法概述
DOI：
--
复制
发表时间：
--
期刊：
影响因子：
--
通讯作者：
W. Fu
中科院分区：
文献类型：
--
作者：
Yanpu Zhao;W. Fu
本文介绍了 Collins Commercial Avionics 和 SRI International 在使用 PVS 验证系统正式指定和验证 AAMP5 微处理器的微代码方面的经验。该项目的目的是确定设计用于实时嵌入式系统的工业微处理器是否可以在指令集和寄存器传输级别上正式指定，以及是否可以使用形式证明来证明微代码的正确性。本文提供了简要的技术概述，但其重点是在使用 PVS 作为这种规模的示例中吸取的经验教训以及在工业环境中使用正式方法的含义。软件和数字硬件越来越多地用于故障可能危及生命的情况，例如飞机、核电站、武器系统和医疗仪器。几位作者已经证明，仅通过测试来证明此类系统满足超高可靠性要求是不可行的[9,19]。形式化方法是增强我们对数字系统信心的一种有前途的方法，但如何在工业环境中有效使用它仍然存在许多问题。本文介绍了一个项目，即 AAMP5 微处理器中微代码的形式化验证，该项目旨在探索如何将规范和验证的形式化技术引入工业流程。项目包括在 SRI [22] 开发的 PVS 语言中指定罗克韦尔专有微处理器 AAMP5 的一部分，在指令集和寄存器传输级别，并使用 PVS 定理证明器来显示微代码正确地实现了代表性指令子集的指定行为。虽然本文包含一个简短的技术概述（详细的技术讨论请参阅[28,29]），但其重点是在使用 PVS 作为这种规模的示例中吸取的经验教训以及在工业环境中使用正式方法的含义。该项目的核心结果是证明正式指定商业微处理器以及使用机械正确性证明来验证微代码的可行性。这一点尤其重要，因为 AAMP5 并不是为形式验证而设计的，而是通过流水线指令执行来提供三倍以上的性能改进，同时保持目标代码与早期的 AAMP2 兼容。因此，AAMP5 是应用形式化方法的最复杂的微处理器之一。另一个关键结果是发现了实际错误和种子错误。两个实际的微代码错误......
This paper describes the experiences of Collins Commercial Avionics and SRI International in formally specifying and verifying the microcode for the AAMP5 microprocessor with the PVS verification system. This project was conducted to determine if an industrial microprocessor designed for use in real–time embedded systems could be formally specified at the instruction set and register transfer levels and if formal proofs could be used to prove the microcode correct. The paper provides a brief technical overview, but its emphasis is on the lessons learned in using PVS for an example of this size and the implications for using formal methods in an industrial setting. Software and digital hardware are increasingly being used in situations where failure could be life threatening, such as aircraft, nuclear power plants, weapon systems, and medical instrumentation. Several authors have demonstrated the infeasibility of showing that such systems meet ultra–high reliability requirements through testing alone [9,19]. Formal methods are a promising approach for increasing our confidence in digital systems, but many questions remain on how it can be used effectively in an industrial setting. This paper describes a project, formal verification of the microcode in the AAMP5 microprocessor, conducted to explore how formal techniques for specification and verification could be introduced into an industrial process. project consisted of specifying in the PVS language developed by SRI [22] a portion of a Rockwell proprietary microprocessor, the AAMP5, at both the instruction set and register–transfer levels and using the PVS theorem prover to show the microcode correctly implemented the specified behavior for a representative subset of instructions. While this paper includes a brief technical overview (see [28,29] for a detailed technical discussion), its emphasis is on the lessons learned in using PVS for an example of this size and the implications for using formal methods in an industrial setting. The central result of this project was to demonstrate the feasibility of formally specifying a commercial microprocessor and the use of mechanical proofs of correctness to verify microcode. This is particularly significant since the AAMP5 was not designed for formal verification, but to provide a more than three fold performance improvement, by pipelining instruction execution, while remaining object code compatible with the earlier AAMP2. As a consequence, the AAMP5 is one of the most complex microprocessors to which formal methods have been applied. Another key result was the discovery of both actual and seeded errors. Two actual microcode errors …