Hardware implementations of divide and square root operations are difficult and high-value targets for formal verification. We describe an approach using the ACL2 theorem prover that has resulted in robust, end-to-end correctness proofs for highly optimized industrial implementations of such operations. Using this approach, we developed initial proofs for divide and square root operations in less than three person-months each. We subsequently proved the correctness of all operations on a floating point divide/square root design and an integer divider implementing up to 128-by-64-bit divides, both highly optimized industrial implementations. These proofs run in minutes per operation and have been straightforward to maintain against design changes. This methodology allows lemmas to be proved about portions of the hardware model, and these lemmas seamlessly composed to complete a top-level proof that the whole operation runs correctly. This decomposition allows fully automatic proof methods to be applied to the portions of the hardware model that capacity allows, and the composition of these portions is amenable to rewriting and other traditional interactive theorem proving methods.

Abstract 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 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 micro-operations, 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.

In recent years, leading microprocessor companies have made huge investments to improve the reliability of their products. Besides expanding their validation and CAD tools teams, they have incorporated formal verification methods into their design flows. Formal verification (FV) engineers require extensive training, and FV tools from CAD vendors are expensive. At first glance, it may seem that FV teams are not affordable by smaller companies. We have not found this to be true. This paper describes the formal verification framework we have built on top of publicly-available tools. This framework gives us the flexibility to work on myriad different problems that occur in microprocessor design.