|
|
|---|
|
|
|
|---|
B. Brock, M. Kaufmann, and J S. Moore, “ACL2
Theorems about Commercial Microprocessors”, in M. Srivas and
A. Camilleri, editors, Formal Methods in Computer-Aided Design
(FMCAD'96), Springer-Verlag, LNCS 1166, pp. 275-293, doi
10.1007/BFb0031816, 1996.
Relevance: early (mid-1990s) applications of ACL2 in
industry (Motorola CAP DSP via operational semantics and the AMD K5 FDIV via
a shallow embedding)
Abstract
ACL2 is a mechanized mathematical logic intended for use in specifying and proving properties of computing machines. In two independent projects, industrial engineers have collaborated with researchers at Computational Logic, Inc. (CLI), to use ACL2 to model and prove properties of state-of-the-art commercial microprocessors prior to fabrication. In the first project, Motorola Inc., and CLI collaborated to specify Motorola's complex arithmetic processor (CAP), a single-chip, digital signal processor (DSP) optimized for communications signal processing. Using the specifications, we proved the correctness of several CAP microcode programs. The second industrial collaboration involving ACL2 was between Advanced Micro Devices, Inc. (AMD) and CLI. In this work we proved the correctness of the kernel of the floating-point division operation on AMD's first Pentium-class microprocessor, the AMD5K86. In this paper, we discuss ACL2 and these industrial applications, with particular attention to the microcode verification work.
This paper contains a good sketch of the Motorola CAP digital signal processor project, from capturing the design as an ACL2 operational model to proving microcode correct with respect to the model. The paper also includes a timeline describing how long different phases of the project took.
The paper also discusses the first use of ACL2, in 1995, to deal with floating-point arithmetic: verifying microcode for floating-point division on AMD's first Pentium-class microprocessor, the AMD5k86. However, the formalization of the division microcode was not via operational semantics but rather a “shallow embedding” of the microcode into ACL2. So while both the CAP project and floating-point project are of great relevance to the use of formal methods in industry, we have stressed the CAP work in this doc topic on operational semantics. For a technical description of the division proof, see J S. Moore, T. Lynch, and M. Kaufmann, “A Mechanically Checked Proof of the Correctness of the Kernel of the AMD5k86 Floating-Point Division Program”, IEEE Transactions on Computers, 47(9), pp. 913-926, Sep., 1998.