Published: 29th October 2018
DOI: 10.4204/EPTCS.280
ISSN: 2075-2180

EPTCS 280

Proceedings of the 15th International Workshop on the
ACL2 Theorem Prover and Its Applications
Austin, Texas, USA, November 5-6, 2018

Edited by: Shilpi Goel and Matt Kaufmann

Preface
Shilpi Goel and Matt Kaufmann
A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java
Alessandro Coglio
1
Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32
Mihir Parang Mehta
18
Trapezoidal Generalization over Linear Constraints
David Greve and Andrew Gacek
30
Incremental SAT Library Integration Using Abstract Stobjs
Sol Swords
47
Using ACL2 in the Design of Efficient, Verifiable Data Structures for High-Assurance Systems
David Hardin and Konrad Slind
61
Adding 32-bit Mode to the ACL2 Model of the x86 ISA
Alessandro Coglio and Shilpi Goel
77
A Toolbox For Property Checking From Simulation Using Incremental SAT (Extended Abstract)
Rob Sumners
95
The Fundamental Theorem of Algebra in ACL2
Ruben Gamboa and John Cowles
98
Real Vector Spaces and the Cauchy-Schwarz Inequality in ACL2(r)
Carl Kwan and Mark R. Greenstreet
111
Convex Functions in ACL2(r)
Carl Kwan and Mark R. Greenstreet
128
Smtlink 2.0
Yan Peng and Mark R. Greenstreet
143
DefunT: A Tool for Automating Termination Proofs by Using the Community Books (Extended Abstract)
Matt Kaufmann
161
Hint Orchestration Using ACL2's Simplifier
Sol Swords
164

Preface

This volume contains the proceedings of the Fifteenth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2018), a two-day workshop held in Austin, Texas, USA, on November 5-6, 2018, immediately after FMCAD (http://www.fmcad.org/FMCAD18), on the University of Texas campus. ACL2 workshops occur at approximately 18-month intervals, and they provide a major technical forum for users of the ACL2 theorem proving system to present research related to the ACL2 theorem prover and its applications.

ACL2 is an industrial-strength automated reasoning system, the latest in the Boyer-Moore family of theorem provers. The 2005 ACM Software System Award was awarded to Boyer, Kaufmann, and Moore for their work in ACL2 and the other theorem provers in the Boyer-Moore family.

The proceedings of ACL2-2018 include eleven long papers and two extended abstracts. Each submission received three reviews. The workshop also included several “rump session” talks — short unpublished presentations that discussed ongoing research — as well as three invited talks:

This workshop would not have been possible without the support of a large number of people. We thank our generous sponsors, Centaur Technology and Oracle Corporation. We thank those who contributed papers, as well as the members of the Program Committee for providing careful reviews and for engaging in lively discussion. We thank the members of the Steering Committee for their help and guidance. We are grateful to the invited speakers for sharing their insights. We thank The University of Texas (UT Austin), Warren Hunt, Jr., and Lindy Aleshire for helping us to get a venue for our workshop. We thank EasyChair, EPTCS, arXiv, and RegOnline for providing assistance with the logistics of the workshop. Thanks are also due to David Rager for helping us administer registration. We are also grateful for support of our time spent on workshop preparations from Centaur Technology, UT Austin, the Kestrel Institute, and DARPA under Contract Nos. FA8650-17-1-7704 and FA8750-15-C-0007. Last, but not least, we thank Mertcan Temel for his assistance with local arrangements. It has been a pleasure and an honor to chair this event.

Shilpi Goel and Matt Kaufmann
November, 2018

ACL2 2018 Program Committee

Harsh Chamarthi Intel
Alessandro Coglio Kestrel Institute
Jared Davis Apple
Ruben Gamboa University of Wyoming
Shilpi Goel Centaur Technology
Dave Greve Rockwell-Collins
Warren Hunt The University of Texas
Sebastiaan Joosten University of Twente
Matt Kaufmann The University of Texas
John O'Leary Intel
Grant Passmore Aesthetic Integration
David Rager Oracle
Sandip Ray University of Florida
David Russinoff ARM
Julien Schmaltz Eindhoven University of Technology
Anna Slobodova Centaur Technology
Eric Smith Kestrel Institute
Sol Swords Centaur Technology

A Toolbox For Property Checking From Simulation Using Incremental SAT (Extended Abstract)

Rob Sumners (Centaur Technology)

Abstract

We present a tool that primarily supports the ability to check bounded properties starting from a sequence of states in a run. The target design is compiled into an AIGNET which is then selectively and iteratively translated into an incremental SAT instance in which clauses are added for new terms and simplified by the assignment of existing literals. Additional applications of the tool can be derived by the user providing alternative attachments of constrained functions which guide the iterations and SAT checks performed. Some Verilog RTL examples are included for reference.

Overview

Formal property verification of modern hardware systems is often too onerous to prove directly with a theorem prover and too expensive to prove with more automatic techniques. A common remedy to this difficulty is to focus on proving properties from a more limited logic (e.g. STE([9]), BMC([2]), using SVTVs([10]) in previous ACL2 work). In these cases, properties are reduced in scope to only consider the effects of a bounded number of next-steps of the transition function of the hardware design; this, in turn, greatly increases the capacity of the hardware designs one can target with automatic propositional logic verification techniques (primarily SAT). The general downside of this reduction in property scope is the need to codify and prove (inductive) invariants of the reachable states of the design. The definition and proof of these invariants is not only time consuming but the invariants are often brittle and require significant maintenance with ongoing design change. An alternative approach is to bypass the definition and proof of invariants and instead check the properties from a set of representative states of the system -- one can then either prove that these states are in fact representative or accept the results of the property checks as a sufficient semi-formal check of the design and disregard a full proof. We briefly cover the design and definition of a tool (named exsim) which builds upon existing hardware verification work in the ACL2 community (VL([7]), SV([10]), AIGNET([3])) to add the capability to efficiently check bounded properties across a sequence of next-states of the design using incremental SAT([13)]). An initial version of the tool and some example Verilog designs and runs are included in the supporting materials.

Figure 1: Simple toy and top module definitions

module toy (input reset, input clk, input op, input [1:0] in, output reg [1:0] out);
...
always@* w1 = tmp|in;
always@* w2 = tmp&{2{in[0]}};
always@(posedge clk) tmp <= in;
always@(posedge clk) out <= (op ? w1 : w2);
endmodule // toy

module top (input reset, input clk, input wave_op, input [1:0] free_in, output fail_out);
...
always@(posedge clk) in <= free_in;
always@(posedge clk) op <= wave_op;
toy des(.*);
always@(posedge clk) fail_out <= &out;
endmodule // top

Design and Toy Example

The exsim function is split into two steps. The first step is the function exsim-prep which reads in a verilog design and compiles it into an AIGNET -- an optimized ``circuit'' representation built from AND and XOR gates and inverters supporting efficient simplification procedures([3]).

The second step of exsim is the function exsim-run which reads in a waveform for the design (from a VCD file) and initializes the data structures needed to iterate through the exsim-main-loop. As part of this initialization, inputs of the design are tagged as either :wave, :rand, or :free corresponding to input values tracking values from the input waveform, being generated randomly, or being left as free variables. In addition, certain signals are tagged as :fail which merely designates these signals as the properties we are checking -- namely that these fail signals never have a non-zero value after reset. A simple toy example in Figure 1 is provided for reference -- the default signal tagging function would tag free_in as the sole :free input and fail_out as the sole :fail signal to check.

The primary function of the exsim-main-loop is to update an incremental SAT instance([1]) such that the clauses in the SAT instance correspond to a check of :fail signals at certain clock cycles having the value of 1 relative to certain values of :free inputs on previous clock cycles. The main-loop iterates through a sequence of operations primarily comprised of :step-fail, :step-free, and :check-fails which respectively add clauses to SAT for the :fail at the next clock cycle, add unit clauses to SAT corresponding to an assignment to :free variables on an earlier clock cycle, and calling the SAT solver to check if any of the :fail signals could be 1 in the current context. The ``compiled'' AIGNET from exsim-prep allows for an efficient implementation of :step-free and :step-fail for larger designs.

The choice of which step to take is heuristic and depends primarily on the current number of clauses in the database. In particular, :step-fail will add clauses to SAT while :step-free will reduce clauses in SAT and heuristics will choose when to perform each action depending on how extensively the user wishes to search for fails in a given instance. The default heuristic choice function (as well as several other functions defining default operation) can be overridden using ACL2's defattach feature([8]).

Returning to our simple toy example from Figure 1. Let's assume that the input wave_op gets a value of 1 at every clock cycle from the input waves. After a sufficient number of :step-fails, this would reduce the check of fail_out being 1 to free_in having at least a single 1 in each bit position over 2 consecutive clocks, 3 clocks earlier.

The intent of the exsim toolkit is to provide the user the capability to control the SAT checks that are performed to optimize effective search capacity over runtime. This is primarily achieved by allowing the user to carefully specify which input variables should be :free (which reduces potential decision space during SAT along with increasing propagations) and when to either extend or reduce the current set of SAT clauses by inspecting the current number of active clauses. The additional benefit of incremental SAT is that the aggregate cost of successive searches is reduced by the sharing of learned reductions.

The exsim toolkit is a work in progress. Current development efforts afford better control over bindings of free variables and more intermediate targets for search (not just :fail signals). Related to these efforts, an earlier proof of ``correctness'' needs to be reworked to keep apace with the design changes. As a note on this ``proof'', the goal is to ensure that each :check-fails which returns UNSAT ensures no possible assignment for the free variables in the scope of the current check. This reduces to proving an invariant relating the current SAT clauses with the values of signals at certain clock cycles.

References

  1. Tomas Balyo, Armin Biere, Markus Iser & Carsten Sinz (2016): SAT Race 2015. Artif. Intell. 241, pp. 45--65, doi:10.1016/j.artint.2016.08.007.
  2. Edmund M. Clarke, Armin Biere, Richard Raimi & Yunshan Zhu (2001): Bounded Model Checking Using Satisfiability Solving. Formal Methods in System Design 19(1), pp. pages7--34, doi:10.1023/A:1011276507260.
  3. Jared Davis & Sol Swords (2013): Verified AIG Algorithms in ACL2. In Gamboa & Davis([4]), pp. 95--110, doi:10.4204/EPTCS.114.8.
  4. Ruben Gamboa & Jared Davis, editors (2013): Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2013, Laramie, Wyoming, USA, May 30-31, 2013. EPTCS 114, doi:10.4204/EPTCS.114.
  5. David A. Greve, Matt Kaufmann, Panagiotis Manolios, J Strother Moore, Sandip Ray, Jose-Luis Ruiz-Reina, Rob Sumners, Daron Vroon & Matthew Wilding (2008): Efficient execution in an automated reasoning environment. J. Funct. Program. 18(1), pp. 15--46, doi:10.1017/S0956796807006338.
  6. David Hardin & Julien Schmaltz, editors (2011): Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, November 3-4, 2011. EPTCS 70, doi:10.4204/EPTCS.70.
  7. Warren A. Hunt, Sol Swords, Jared Davis & Anna Slobodova (2010): Use of Formal Verification at Centaur Technology, pp. 65--88. Springer US, addressBoston, MA, doi:10.1007/978-1-4419-1539-9_3.
  8. Matt Kaufmann & J Strother Moore (2014): Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4. In Verbeek & Schmaltz ([12]), pp. 1--7, doi:10.4204/EPTCS.152.1.
  9. Manish Pandey & Randal E. Bryant (1999): Exploiting symmetry when verifying transistor-level circuits by symbolic trajectory evaluation. IEEE Trans. on CAD of Integrated Circuits and Systems 18(7), pp. 918--935, doi:10.1109/43.771176.
  10. Anna Slobodova, Jared Davis, Sol Swords & Warren A. Hunt Jr. (2011): A flexible formal verification framework for industrial scale validation. In: 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign, MEMOCODE 2011, Cambridge, UK, 11-13 July, 2011, pp. 89--97, doi:10.1109/MEMCOD.2011.5970515.
  11. Sol Swords & Jared Davis (2011): Bit-Blasting ACL2 Theorems. In Hardin & Schmaltz ([6]), pp. 84--102, doi:10.4204/EPTCS.70.7.
  12. Freek Verbeek & Julien Schmaltz, editors (2014): Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014. EPTCS 152, doi:10.4204/EPTCS.152.
  13. Jesse Whittemore, Joonyoung Kim & Karem A. Sakallah (2001): SATIRE: A New Incremental Satisfiability Engine. In: Proceedings of the 38th Design Automation Conference, DAC 2001, Las Vegas, NV, USA, June 18-22, 2001, pp. 542--545, doi:10.1145/378239.379019.