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.

We present a hybrid methodology for the formal verification of arithmetic RTL designs that combines sequential logic equivalence checking with interactive theorem proving in a two-step process. First, an intermediate model of the design is extracted by hand and coded in Restricted Algorithmic C, a simple C subset augmented by the C++ register class templates of Algorithmic C, which provide the bit manipulation features of Verilog. The model is designed to mirror the RTL microarchitecture closely enough to allow efficient equivalence checking, but sufficiently abstract to be amenable to formal analysis. The model is then automatically translated to the logic of the ACL2 theorem prover, which is used to establish correctness with respect to an architectural specification. As an illustration, we describe the modeling and proof of correctness of a chained multiply-add module, designed to test techniques for area and power reduction and intended for implementation in future Arm graphics nrocessors.