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.