Published: 18th September 2015
DOI: 10.4204/EPTCS.192
ISSN: 2075-2180


Proceedings Thirteenth International Workshop on the
ACL2 Theorem Prover and Its Applications
Austin, Texas, USA, 1-2 October 2015

Edited by: Matt Kaufmann and David L. Rager

Extended Abstract: A Brief Introduction to Oracle's Use of ACL2 in Verifying Floating-point and Integer Arithmetic
David L. Rager, Jo Ebergen, Austin Lee, Dmitry Nadezhin, Ben Selfridge and Cuong K. Chau
Fix Your Types
Sol Swords and Jared Davis
Second-Order Functions and Theorems in ACL2
Alessandro Coglio
Fourier Series Formalization in ACL2(r)
Cuong K. Chau, Matt Kaufmann and Warren A. Hunt Jr.
Perfect Numbers in ACL2
John Cowles and Ruben Gamboa
Extending ACL2 with SMT Solvers
Yan Peng and Mark Greenstreet
Reasoning About LLVM Code Using Codewalker
David S. Hardin
Stateman: Using Metafunctions to Manage Large Terms Representing Machine States
J Strother Moore
Proving Skipping Refinement with ACL2s
Mitesh Jain and Panagiotis Manolios


This volume contains the proceedings of the Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, ACL2 2015, a two-day workshop held in Austin, Texas, USA, on October 1-2, 2015. ACL2 workshops occur at approximately 18-month intervals and provide a major technical forum for researchers to present and discuss improvements and extensions to the theorem prover, comparisons of ACL2 with other systems, and applications of ACL2 in formal verification.

ACL2 is a state-of-the-art automated reasoning system that has been successfully applied in academia, government, and industry for specification and verification of computing systems and in teaching computer science courses. In 2005, Boyer, Kaufmann, and Moore were awarded the 2005 ACM Software System Award for their work on ACL2 and the other theorem provers in the Boyer-Moore family.

The proceedings of ACL2 2015 include the eight technical papers and one extended abstract that were presented at the workshop. Each submission received at least three reviews. The workshop also included two invited talks: Lessons Learned over 45 Years in Theorem Proving, by J Strother Moore, and Verification in the Age of Integration, by John O'Leary. The workshop also included several rump sessions discussing ongoing research and a panel discussion about the use of ACL2 within industry.

We thank the members of the Program Committee and their sub-reviewers for providing careful and detailed reviews of all the papers. We thank the members of the Steering Committee for their help and guidance. We thank EasyChair for the use of its excellent conference management system. We thank EPTCS and the arXiv for publishing the workshop proceedings in an open-access format.

Matt Kaufmann and David L. Rager
October 2015

Program Chairs

Matt Kaufmann
David L. Rager

Program Committee

Rob Arthan Lemma 1 Ltd.
Jared Davis Centaur Technology Inc.
Ruben Gamboa University of Wyoming
David Greve Rockwell Collins Inc.
David Hardin Rockwell Collins Inc.
Marijn Heule The University of Texas at Austin
Warren A. Hunt, Jr. The University of Texas at Austin
Matt Kaufmann The University of Texas at Austin
Panagiotis Manolios Northeastern University
Francisco Jesús Martín Mateos University of Sevilla
John O'Leary Intel Corporation
Sam Owre SRI International
David L. Rager Oracle Corporation
Sandip Ray Intel Corporation
Julien Schmaltz Eindhoven University of Technology
Anna Slobodova Centaur Technology Inc.
Eric Smith Kestrel Institute
Freek Verbeek Open University of The Netherlands

Additional Reviewers

Coglio, Alessandro

A Brief Introduction to Oracle's Use of ACL2 in Verifying Floating-point and Integer Arithmetic

David L. Rager (Oracle Corporation)
Jo Ebergen (Oracle Corporation)
Austin Lee (Oracle Corporation)
Dmitry Nadezhin (Oracle Corporation)
Ben Selfridge (Oracle Corporation)
Cuong K. Chau (The University of Texas at Austin)

Oracle has developed new implementations for floating-point division and square root and integer division. The Oracle implementations are a variant of the Goldschmidt algorithm [3], an algorithm that serves as the basis for a different AMD K7 implementation [2] and other processors. Our task was to verify the correctness of these implementations all the way down to the Verilog by showing bit-for-bit equivalence with the IEEE 754 Standard on floating-point arithmetic and the integer divide specification in the SPARC ISA. Performing such verifications involved many steps:

This work is similar in spirit to work done by AMD [2], Centaur [4], and others.


We wanted to make as few assumptions as reasonably possible, and we wanted as much of what we did to be mechanically checked. As such, it was important to reason directly about the Verilog -- not just an abstraction of the Verilog created by hand that would then have to be maintained every time the Verilog changed. If the implementation changes in a subtle and incorrect way, we wanted our proofs to break!

We used the ACL2 System and Libraries [1] to symbolically simulate the circuit and verify its correctness. Specifically, we used the GL system to quickly reason about finite objects (i.e., bit vectors). We used the VL 2014 Parser to parse the Verilog, and we used Esim to determine the semantics of the resulting parse trees. Finally, we used the Symbolic Test Vector (STV) framework to initialize values of the circuit and provide the timing abstractions necessary to reason about values that the circuit receives as input and returns as output.

Algorithm Extraction

The Goldschmidt algorithm consists of a repetition of multiplications, additions, and bit-wise complements. We wanted the person verifying the Goldschmidt algorithm against our specifications to be able to reason in terms of these high-level primitives (as opposed to reasoning about nand's and nor's). As such, we proved that various compositions of low-level operations implement these higher-level mathematical operations. We found the GL system to be very helpful in many of these proofs, but GL (really, BDDs and SAT solvers) could not automatically prove all of the necessary abstractions. For example, we used traditional ACL2 rewriting to reason about the composition of Booth encoders and CSA trees to implement multiplication.

Algorithm Verification

Our final task was to show that the aforementioned series of mathematical operations implemented the IEEE 754 specification of floating-point division and square root and our specification for integer division. This first required writing such specifications, which we validated against millions of concrete test vectors. We then proved that the series of mathematical operations from the algorithm extraction implement these specifications. This proof was a sizable effort.


At the end of it all, we have proved, under some assumptions, that the Verilog matches bit for bit with our extracted algorithm. We have also proved that the extracted algorithm satisfies the IEEE floating-point division and square root specifications and the integer division specifications. Thus, transitively, we know that the Verilog implements these specifications.

We discovered no errors with respect to the complete IEEE specification (including exceptions, denormals, and special values) in the Verilog design. As a result, we know, for example, that we have neither omitted an entry from our lookup table, nor accidentally fused together a wire in our multiplier.

Despite the absence of RTL errors, this verification effort was still necessary because there was simply no other way to obtain a reasonable amount of coverage. Another benefit of our work was the discovery of several optimizations, which were all implemented and proven correct. Our thorough error analysis led to an optimization in the lookup tables for division and square root, yielding a reduction of 75% and 50% in the two lookup tables, respectively. Other optimizations led to simplifications in the hardware and in the proof. We look forward to reporting on these at a later date.


We thank Jeff Brooks, Greg Grohoski, Warren Hunt, Matt Kaufmann, Govind Murugan, Chris Olson, and Greg A. Smith for their technical help and support.


  1. ACL2 (2015): ACL2 Documentation. Http://
  2. S.F. Oberman (1999): Floating point division and square root algorithms and implementation in the AMD-K7TM microprocessor. In: Computer Arithmetic, 1999. Proceedings. 14th IEEE Symposium on, pp. 106–115, doi:10.1109/ARITH.1999.762835.
  3. S.F. Oberman & M. Flynn (1997): Division algorithms and implementations. Computers, IEEE Transactions on 46(8), pp. 833–854, doi:10.1109/12.609274.
  4. A. Slobodova, J. Davis, S. Swords & W. Hunt (2011): A flexible formal verification framework for industrial scale validation. In: Formal Methods and Models for Codesign (MEMOCODE), 2011 9th IEEE/ACM International Conference on, pp. 89–97, doi:10.1109/MEMCOD.2011.5970515.