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.

We present a comprehensive, self-contained, and mechanically verified proof of correctness of a maximally redundant SRT design for floating-point division and square root extraction, supported by verified procedures that 1) test the admissibility of a proposed digit selection table, 2) determine the minimal dimensions of an admissible table for a given arbitrary radix, and 3) generate these tables. For square root extraction, we also provide a verified procedure for generating an initial approximation that meets the accuracy requirement of the algorithm and ensures that the digit selection index derived from successive partial roots remains static throughout the computation. A radix-8 instantiation of these algorithms has been implemented in the floating-point unit of the AMD processor code-named Steamroller. To ensure their correctness, all of our results and procedures have been formalized and mechanically checked by the ACL2 prover. We present evidence of the value of this approach by comparing it to that of a more conventional published paper that reports similar results, which are shown to be fatally flawed.

Abstract As an application of a system designed for concurrent program verification, we describe a formalisation and mechanical proof of the correctness of Ben-Ari's incremental garbage collection algorithm. The proof system is based on the Manna-Pnueli model of concurrency and is implemented as an extension of the Boyer-Moore prover. The correctness of the garbage collector is represented by two theorems, stating a) that nothing except garbage is ever collected (safety), and b) that all garbage is eventually collected (liveness). We compare our mechanised treatment with several published proofs of the same results.