|
Published: 29th October 2018 DOI: 10.4204/EPTCS.280 ISSN: 2075-2180 |
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 |
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.
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.
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
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.