Major Section: ACL2-TUTORIAL
ACL2 is an interactive system in which you can model digital artifacts and guide the system to mathematical proofs about the behavior of those models. It has been used at such places as AMD, Centaur, IBM, and Rockwell Collins to verify interesting properties of commercial designs. It has been used to verify properties of models of microprocessors, microcode, the Sun Java Virtual Machine, operating system kernels, other verifiers, and interesting algorithms.
Here we list just a few of the industrially-relevant results obtained with ACL2. Reading the list may help you decide you want to learn how to use ACL2. If you do decide you want to learn more, we recommend that you take The Tours after you leave this page.
ACL2 was used at Motorola Government Systems to certify several microcode programs for the Motorola CAP digital signal processor, including a comparator sort program that is particularly subtle. In the same project, ACL2 was used to model the CAP at both the pipelined architectural level and the instruction set level. The architectural model was bit- and cycle-accurate: it could be used to predict every bit of memory on every cycle. The models were proved equivalent under certain hypotheses, the most important being a predicate that analyzed the microcode for certain pipeline hazards. This predicate defined what the hazards were, syntactically, and the equivalence of the two models established the correctness of this syntactic characterization of hazards. Because ACL2 is a functional programming language, the ACL2 models and the hazard predicate could be executed. ACL2 executed microcode interpretr several times faster than the hardware simulator could execute it -- with assurance that the answers were equivalent. In addition, the ACL2 hazard predicate was executed on over fifty microcode programs written by Motorola engineers and extracted from the ROM mechanically. Hazards were found in some of these. (See, for example, Bishop Brock and Warren. A. Hunt, Jr. ``Formal analysis of the motorola CAP DSP.'' In Industrial-Strength Formal Methods. Springer-Verlag, 1999.)
ACL2 was used at Advanced Micro Devices (AMD) to verify the compliance of the AMD Athon's (TM) elementary floating point operations with their IEEE 754 specifications. This followed ground-breaking work in 1995 when ACL2 was used to prove the correctness of the microcode for floating-point division on the AMD K5. The AMD Athlon work proved addition, subtraction, multiplication, division, and square root compliant with the IEEE standard. Bugs were found in RTL designs. These bugs had survived undetected in hundreds of millions of tests but were uncovered by ACL2 proof attempts. The RTL in the fabricated Athlon FPU has been mechanically verified by ACL2. Similar ACL2 proofs have been carried out for every major AMD FPU design fabricated since the Athlon. (See for example, David Russinoff. ``A mechanically checked proof of correctness of the AMD5K86 floating-point square root microcode''. Formal Methods in System Design Special Issue on Arithmetic Circuits, 1997.)
ACL2 was used at IBM to verify the floating point divide and square root on the IBM Power 4. (See Jun Sawada. ``Formal verification of divide and square root algorithms using series calculation''. In Proceedings of the ACL2 Workshop 2002, Grenoble, April 2002.)
ACL2 was used to verify floating-point addition/subtraction instructions for the media unit from Centaur Technology's 64-bit, X86-compatible microprocessor. This unit implements over one hundred instructions, with the most complex being floating-point addition/subtraction. The media unit can add/subtract four pairs of floating-point numbers every clock cycle with an industry-leading two-cycle latency. The media unit was modeled by translating its Verilog design into an HDL deeply embedded in the ACL2 logic. The proofs used a combination of AIG- and BDD-based symbolic simulation, case splitting, and theorem proving. (See Warren A. Hunt, Jr. and Sol Swords. ``Centaur Technology Media Unit Verification''. In CAV '09: Proceedings of the 21st International Conference on Computer Aided Verification, pages 353--367, Berlin, Heidelberg, 2009. Springer-Verlag.)
Rockwell Collins used ACL2 to prove information flow properties about its Advanced Architecture MicroProcessor 7 Government Version (AAMP7G), a Multiple Independent Levels of Security (MILS) device for use in cryptographic applications. The AAMP7G provides MILS capability via a verified secure hardware-based separation kernel. The AAMP7G's design was proved to achieve MILS using ACL2, in accordance with the standards set by EAL-7 of the Common Criteria and Rockwell Collins has received National Security Agency (NSA) certification for the device based on this work. (See David S. Hardin, Eric W. Smith, and William. D. Young. ``A robust machine code proof framework for highly secure applications''. In Proceedings of the sixth international workshop on the ACL2 theorem prover and its applications, pages 11--20, New York, NY, USA, 2006. ACM.)
Key properties of the Sun Java Virtual Machine and its bytecode verifier were verified in ACL2. Among the properties proved were that certain invariants are maintained by class loading and that the bytecode verifier insures that execution is safe. In addition, various JVM bytecode programs have been verified using this model of the JVM. (See Hanbing Liu. Formal Specification and Verification of a JVM and its Bytecode Verifier. PhD thesis, University of Texas at Austin, 2006.)
The Boyer-Moore fast string searching algorithm was verified with ACL2, including a model of the JVM bytecode for the search algorithm itself (but not the preprocessing). (See J S. Moore and Matt Martinez. ``A mechanically checked proof of the correctness of the Boyer-Moore fast string searching algorithm.'' In Engineering Methods and Tools for Software Safety and Security pages 267--284. IOS Press, 2009.)
ACL2 was used to verify the fidelity between an ACL2-like theorem prover and a simple (``trusted by inspection'') proof checker, thereby establishing (up to the soundness of ACL2) the soundness of the ACL2-like theorem prover. This project was only part of a much larger project in which the resulting ACL2 proof script was then hand-massaged into a script suitable for the ACL2-like theorem prover to process, generating a formal proof of its fidelity that has been checked by the trusted proof checker. (See Jared Davis. Milawa: A Self-Verifying Theorem Prover. Ph.D. Thesis, University of Texas at Austin, December, 2009.)
These are but a few of the interesting projects carried out with ACL2. Many of the authors mentioned above have versions of the papers on their web pages. In addition, see the link to ``Books and Papers about ACL2 and Its Applications'' on the ACL2 home page (http://www.cs.utexas.edu/users/moore/acl2). Also see the presentations in each of the workshops listed in the link to ``ACL2 Workshops'' on the ACL2 home page.
