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:

- Reduce the level of human understanding needed in the initial process of developing the proof;
- Provide clear counterexamples, whereas failed ACL2 proofs can often be difficult to debug; and
- Ease the maintenance of the proof, since after the design changes they can often find updated proofs without help.

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.

- Term-level-reasoning
- GL's term-level proof support
- Glmc
- ACL2 interface to AIG-based safety model checking
- Other-resources
- Additional resources (talks, academic papers, a dissertation) for learning about GL.
- Optimization
- How to optimize GL's symbolic simulations for faster or larger-scale proofs.
- Reference
- Reference documentation for using GL.
- Debugging
- Advice and tools for debugging performance problems and failed gl proofs.
- Basic-tutorial
- An introductory guide, recommended for new users of gl.