Some industrial examples of ACL2 use

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

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 a microcode interpreter 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 Athlon**'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
Matthew M. Wilding, David A. Greve, Raymond J. Richards, and David S. Hardin.
``Formal Verification of Partition Management for the AAMP7G
Microprocessor''. In *Design and Verification of Microprocessor Systems for
High-Assurance Applications*, David S. Hardin, ed., pages 175–191,
Springer US, 2010.)

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 ensures 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 Books and Papers about ACL2 and its Applications. Also, see the presentations in each of the ACL2 Workshops.