Preface

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

Program Committee

Additional Reviewers

Coglio, Alessandro

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

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:

• Parsing the Verilog and bringing the design into the ACL2 logic -- parsing,
• Abstracting low-level bit-oriented primitives, (e.g., nands, nors, muxes, etc.) to higher-level data types and mathematical operations like addition and multiplication -- algorithm extraction, and
• Proving that sequences of these mathematical operations satisfy the IEEE 754 and Integer Divide specifications -- algorithm verification.

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

Parsing

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.

Results

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.

Acknowledgements

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

References

1. ACL2 (2015): ACL2 Documentation. Http://www.cs.utexas.edu/users/moore/acl2/v7-1/combined-manual/.
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.