Published: 2nd May 2017
DOI: 10.4204/EPTCS.249
ISSN: 2075-2180

EPTCS 249

Proceedings 14th International Workshop on the
ACL2 Theorem Prover and its Applications
Austin, Texas, USA, May 22-23, 2017

Edited by: Anna Slobodova and Warren Hunt Jr.

Preface
Warren Hunt Jr. and Anna Slobodova
The x86isa Books: Features, Usage, and Future Plans
Shilpi Goel
1
The Cayley-Dickson Construction in ACL2
John Cowles and Ruben Gamboa
18
A Computationally Surveyable Proof of the Group Properties of an Elliptic Curve
David M. Russinoff
30
Meta-extract: Using Existing Facts in Meta-reasoning
Matt Kaufmann and Sol Swords
47
A Versatile, Sound Tool for Simplifying Definitions
Alessandro Coglio, Matt Kaufmann and Eric W. Smith
61
Proof Reduction of Fair Stuttering Refinement of Asynchronous Systems and Applications
Rob Sumners
78
Term-Level Reasoning in Support of Bit-blasting
Sol Swords
95
Extended Abstract: Formal Specification and Verification of the FM9001 Microprocessor Using the DE System
Cuong Chau
112

Preface

This volume contains the proceedings of the Fourteenth International Workshop on the ACL2 Theorem Prover and Its Applications, ACL2 2017, a two-day workshop held in Austin, Texas, USA, on May 22-23, 2017. ACL2 workshops occur at approximately 18-month intervals, and they provide a 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. 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 theorem-prover family.

The proceedings of 2017 ACL2 Workshop include the seven technical papers and one extended abstract that were presented at the workshop. Each submission received two or three reviews. The workshop also included three invited talks: Using Mechanized Mathematics in an Organization with a Simulation-Based Mentality, by Glenn Henry of Centaur Technology, Inc.; Formal Verification of Financial Algorithms, Progress and Prospects, by Grant Passmore of Aesthetic Integration; and Verifying Oracle's SPARC Processors with ACL2 by Greg Grohoski of Oracle. The workshop also included several rump sessions discussing ongoing research and 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. And we thank EPTCS and the arXiv for publishing the workshop proceedings in an open-access format. We also like to thank Centaur Technology and Oracle Corporation for their generous sponsorship of the workshop.

Warren A. Hunt, Jr. and Anna Slobodova
May, 2017

ACL2 2017 Program Committee

          Alessandro Coglio        Kestrel Institute
          John Cowles              University of Wyoming
          Mark Greenstreet         University of British Columbia
          David Greve              Rockwell-Collins, Inc.
          David Hardin             Rockwell-Collins, Inc.
          Warren Hunt, Jr.         University of Texas
          Matt Kaufmann            University of Texas
          Pete Manolios            Northeastern University
          J Moore                  University of Texas
          Rex Page                 University of Oklahoma
          Dmitry Nadezhin          Oracle Corporation
          David Rager              Oracle Corporation
          Sandip Ray               NXP Semiconductors
          Jose-Luis Ruiz-Reina     University of Seville
          David Russinoff          ARM, Inc.
          Anna Slobodova           Centaur Technology, Inc.
          Rob Sumners              Centaur Technology, Inc.
          Freek Verbeek            Open University, The Netherlands


Additional Reviewers

          Marc Schoolderman        Radbound University Nijmegen,
                                   The Netherlands

Extended Abstract: Formal Specification and Verification of the FM9001 Microprocessor Using the DE System

Cuong Chau (The University of Texas at Austin)

We present our work on formally specifying and mechanically verifying the correctness of the FM9001 microprocessor design using the DE system. The FM9001 microprocessor design was originally specified and verified in the Nqthm logic by Brock and Hunt using the DUAL-EVAL system, the precursor of DE. The main challenge is that ACL2 does not support Nqthm's shell principle, which is used in the original work to formalize the memory model. Instead we represent a memory cell as a proper list of two elements in which the first element is a flag specifying the memory type of the cell, and the second element is a four-valued vector representing the value of that memory cell. This memory representation does not affect the proof strategy for FM9001 created in the previous work, except for establishing the monotonicity property of a netlist's module, which is part of the FM9001 verification procedure. The reason is because the state approximation notion is changed under our proposed representation of the memory model. By modifying the state approximation definition, we successfully prove that the monotonicity property for a module still holds using stricter hypotheses, and finally prove that the FM9001 microprocessor design is correct with respect to a behavioral specification.

Overview

The FM9001 microprocessor design was originally specified and verified in the Nqthm logic by Brock and Hunt using the DUAL-EVAL system ([2]). We attempt to re-specify and re-verify the FM9001 netlist in the ACL2 logic using the DE system. The DE language is similar in spirit and syntax to the DUAL-EVAL language, but they are different in a number of subtle aspects ([3]). In addition, along with our work on the FM9001 specification and verification, we also verify guards for the DE system.

Our verification of the FM9001 microprocessor basically follows the same approach as presented by Brock and Hunt. We basically follow the same proof strategy as done in the previous work. However, there are some lemmas for which we have to come up with a different strategy to prove since the previous strategy does not work in ACL2.

As in the previous work, we heavily use macros for the purpose of automating our framework. The problem is that we are unable to reuse the macros from the previous work since they were defined in Common Lisp. They used features that are not supported in ACL2. Hence we have to define our own macros in ACL2, which requires a fair amount of effort.

The main challenge in our verification of FM9001 is that we are unable to represent the memory model for FM9001 using the shell principle as done in the previous work, since there is no such principle in ACL2. Specifically, the FM9001 memory was modeled using tree structures, with values stored at the tips. It was modeled in the Nqthm logic by using the shell principle to introduce three shells: the shell constructor ROM tags read-only locations of the memory, while the shell constructor RAM tags read-write locations and the shell constructor STUB represents "unimplemented" portions. Each instance of the memory parts includes a value, which is returned when that memory location is read. As mentioned, we are unable to represent the memory model in ACL2 using the shell principle. Instead we represent a memory cell as a proper list of two elements in which the first element is a flag specifying the memory type of the cell (i.e., ROM, or RAM, or STUB), and the second element is the value of that memory cell. This memory representation does not affect the proof strategy for FM9001 created in the previous work, except for establishing the monotonicity property of a netlist's module, which is part of the FM9001 verification procedure. The reason is because the state approximation notion is changed under our proposed representation of the memory model. Below is the ACL2 version of the state approximation definition introduced in the previous work.

(defun s-approx (s1 s2) (cond ((or (consp s1) (consp s2)) // (1) (if (consp s1) (if (consp s2) (and (s-approx (car s1) (car s2)) (s-approx (cdr s1) (cdr s2))) nil) nil)) ((or (ramp s1) (ramp s2)) ...) // (2) ((or (romp s1) (romp s2)) ...) // (3) ((or (stubp s1) (stubp s2)) ...) // (4) (t ...))) // (5)

Since our model constructs memory cells as CONSES; cases (2), (3), and (4) in the above definition will never be satisfied. They are all subsumed in case (1). We are now forced to change the state approximation definition above by rearranging the order of cases to (2), (3), (4), (1), and (5). We also need the following property in order to establish the monotonicity property for a module.

(implies (s-approx s1 s2) (s-approx (cdr s1) (cdr s2)))

This property holds when we impose a constraint on the value of each memory cell that it must be a four-valued vector. This constraint does not change the correctness proofs for FM9001 because the FM9001 specification enforces a restriction that only bit vectors are stored in memory. After obtaining the above property, we then manage to establish the monotonicity property for a module using stricter hypotheses. In particular, the monotonicity property now requires the structure of the module's state and the structure of the netlist containing the module to be well-formed.

Conclusion

While our modeling of the memory model for FM9001 is not the same as in the previous work, we successfully verify the correctness the FM9001 microprocessor design. This work provides a library of verified hardware circuit generators that can be applied when reasoning about the synthesis of hardware circuits. This work is also a contribution to ACL2 for two reasons. First, it moves into the ACL2 regression suite one of the most important theorems proved by Nqthm. Second, it is the first step toward porting the entire Computational Logic verified stack ([1, 4]) from Nqthm to ACL2. We hope others will take the subsequent steps.

References

  1. W. R. Bevier, W. A. Hunt, Jr., J S. Moore & W. D. Young (1989): Special Issue on System Verification. Journal of Automated Reasoning 5(4), pp. 409–530.
  2. B. Brock & W. Hunt (1997): The DUAL-EVAL Hardware Description Language and Its Use in the Formal Specification and Verification of the FM9001 Microprocessor. In: Journal of Formal Methods in System Design 11. Kluwer Academic Publishers, pp. 71–104, doi:10.1023/A:1008685826293.
  3. W. Hunt (2000): The DE Language. In: M. Kaufmann, P. Manolios & J S. Moore: Computer-Aided Reasoning: ACL2 Case Studies, chapter 10. Springer US, pp. 151–166, doi:10.1007/978-1-4757-3188-0_10.
  4. J S. Moore (1996): Piton: A Mechanically Verified Assembly-Level Language. Automated Reasoning Series, Kluwer Academic Publishers.