Published: 18th September 2015 DOI: 10.4204/EPTCS.192 ISSN: 2075-2180 |
Preface | |
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 | 1 |
Fix Your Types Sol Swords and Jared Davis | 3 |
Second-Order Functions and Theorems in ACL2 Alessandro Coglio | 17 |
Fourier Series Formalization in ACL2(r) Cuong K. Chau, Matt Kaufmann and Warren A. Hunt Jr. | 35 |
Perfect Numbers in ACL2 John Cowles and Ruben Gamboa | 53 |
Extending ACL2 with SMT Solvers Yan Peng and Mark Greenstreet | 61 |
Reasoning About LLVM Code Using Codewalker David S. Hardin | 79 |
Stateman: Using Metafunctions to Manage Large Terms Representing Machine States J Strother Moore | 93 |
Proving Skipping Refinement with ACL2s Mitesh Jain and Panagiotis Manolios | 111 |
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
Matt Kaufmann |
David L. Rager |
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 |
Coglio, Alessandro
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.
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.
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.