Formal methods are becoming an indispensable part of the design process in software and hardware industry. It takes robust tools and proofs to make formal validation of large scale projects reliable. In this paper, we...
详细信息
ISBN:
(纸本)9783030816858;9783030816841
Formal methods are becoming an indispensable part of the design process in software and hardware industry. It takes robust tools and proofs to make formal validation of large scale projects reliable. In this paper, we will describe the current status of formal verification at Centaur Technology. We will explain our challenges and our methodology how various proofs and verification artifacts are interconnected and how we keep them consistent over the duration of a project. We also describe our main engine a powerful symbolic simulator with rewriting capabilities that is integrated in a theorem prover and proven correct.
verification of modern microprocessors is a complex task that requires a substantial allocation of resources. Despite significant progress in formal verification, the goal of complete verification of an industrial des...
详细信息
ISBN:
(纸本)9781450370974
verification of modern microprocessors is a complex task that requires a substantial allocation of resources. Despite significant progress in formal verification, the goal of complete verification of an industrial design has not been achieved. In this paper, we describe a current contribution of formal methods to the validation of modern x86 microprocessors at Centaur Technology. We focus on proving correctness of instruction implementations, which includes the decoding of an instruction, its translation into a sequence of microoperations, any subsequent execution of traps to microcode ROM, and the implementation of these micro-operations in execution units. All these tasks are performed within one verification framework, which includes a theorem prover, a verified symbolic simulator, and SAT solvers. We describe the work of defining the needed formal models for both the architecture and micro-architecture in this framework, as well as tools for decomposing the requisite properties into smaller lemmas which can be automatically checked. We additionally cover the advantages and limitations of our approach. To our knowledge, there are no similar results in the verification of implementations of an x86 microprocessor.
ACL2 is a reimplemented extended version of Boyer and Moore's Nqthm and Kaufmann's Pc-Nqthm, intended for large scale verification projects. This paper deals primarily with how we scaled up Nqthm's logic t...
详细信息
ACL2 is a reimplemented extended version of Boyer and Moore's Nqthm and Kaufmann's Pc-Nqthm, intended for large scale verification projects. This paper deals primarily with how we scaled up Nqthm's logic to an ''industrial strength'' programming language-namely, a large applicative subset of Common Lisp-while preserving the use of total functions within the logic. This makes it possible to run formal models efficiently while keeping the logic simple. We enumerate many other important features of ACL2 and we briefly summarize two industrial applications: a model of the Motorola GAP digital signal processing chip and the proof of the correctness of the kernel of the floating point division algorithm on the AMD5(K)86 microprocessor by Advanced Micro Devices, Inc.
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 regar...
详细信息
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.
暂无评论