|
|
|---|
|
|
|
|---|
A symbolic simulation framework for proving finitely bounded ACL2 theorems by bit-blasting with a Binary Decision Diagram (BDD) package or a SAT solver.
GL is a convenient and efficient tool for solving many finite ACL2 theorems that arise in hardware-verification and other contexts. It has played an important role in the verification of arithmetic units and microcode routines at Centaur Technology.
GL makes extensive use of hons-and-memoization. Some
optional parts of GL also require
GL translates ACL2 problems into Boolean problems that can be solved by automatic boolean-reasoning tools. When this approach can be used, there are some good reasons to prefer it over the-method of traditional, interactive theorem proving. For instance, it can:
How does this translation work? You can probably imagine writing a bit-based encoding of ACL2 objects. For instance, you might represent an integer with some structure that contains a 2's-complement list of bits. GL uses an encoding like this, except that Boolean expressions take the place of the bits. We call these structures symbolic-objects.
GL provides a way to effectively compute with symbolic objects; e.g., it can "add" two integers whose bits are expressions, producing a new symbolic object that represents their sum. GL can perform similar computations for most ACL2 primitives. Building on this capability, it can symbolically execute terms. The result of a symbolic execution is a new symbolic object that captures all the possible values the result could take.
Symbolic execution can be used as a proof procedure. To prove a
theorem, we first symbolically execute its goal formula, then show the
resulting symbolic object cannot represent
New users should begin with the basic-tutorial, which walks through the basic ideas behind how GL works, and includes some examples that cover how to use GL.
Once you start to use GL, you will likely be interested in the reference section of this documentation.
Like any automatic procedure, GL has a certain capacity. But when these limits are reached, you may be able to work around the problem in various ways. The optimization section explains various ways to improve GL's performance.
Occasionally GL proofs will fail due to resource limitations or limitations of its symbolic evaluation strategy. When you run into problems, you may be interested in some tools and techniques for debugging failed proofs.
If you want to go further with GL, you will probably want to explore other-resources beyond just this documentation, which include Sol Swords' Ph.D. dissertation, as well as many other academic papers and talks.