Other-resources
Additional resources (talks, academic papers, a dissertation) for
learning about GL.
Besides this xdoc documentation, most GL users will
probably want to be aware of at least the following resources:
- Sol Swords and Jared Davis. Bit-Blasting ACL2 Theorems.
In ACL2 Workshop 2011. November, 2011. EPTCS 70. Pages 84-102.
- This is an approachable, user-focused introduction to GL as of 2011, which
also contains many pointers to related work. It's probably a good idea to read
this first, noting that a few details have changed. Much of this paper has now
been incorporated into this xdoc documentation.
- Sol Swords. A
Verified Framework for Symbolic Execution in the ACL2 Theorem Prover.
Ph.D. thesis, University of Texas at Austin. December, 2010.
- This is the most comprehensive guide to GL's internals. It covers tricky
topics like the handling of if statements and the details of BDD
parametrization. It also covers the logical foundations of GL, such as
correctness claims for symbolic counterparts, the introduction of symbolic
interpreters, and the definition and verification of the GL clause processor.
Some topics are now somewhat dated, but it is good general background for
anyone who wants to extend GL.
- The documentation for hons-and-memoization.
- GL makes heavy use of hash consing and memoization. GL users will likely
want to be aware of the basics of hons-and-memoization, and of commands
like hons-summary, hons-wash, and set-max-mem.
Back-end Solvers
- Jared Davis and Sol Swords. Verified AIG Algorithms in
ACL2. In ACL2 Workshop 2013. May, 2013. EPTCS 114. Pages 95-110.
- This is a more recent paper that's not especially focused on GL, but which
covers aignet and satlink, which can be used by
GL in its new gl-satlink-mode. Many problems that are difficult to
solve using ubdds can be solved using satlink.
- Sol Swords and Warren A Hunt, Jr. A Mechanically Verified
AIG to BDD Conversion Algorithm. In ITP 2010, LNCS 6172, Springer. Pages
435-449.
- This is an older paper about the details of the bddify algorithm that
is used as the engine for gl-aig-bddify-mode.
GL Applications
GL has been used at Centaur Technology to verify RTL implementations of
floating-point addition, multiplication, and conversion operations, as well as
hundreds of bitwise and arithmetic operations on scalar and packed integers.
Some papers describing some of this work include:
- Anna Slobodova, Jared Davis, Sol Swords, and Warren A. Hunt, Jr. A Flexible Formal
Verification Framework for Industrial Scale Validation. In Memocode 2011,
IEEE. Pages 89-97.
- Warren A. Hunt, Jr., Sol Swords, Jared Davis, and Anna Slobodova. Use
of Formal Verification at Centaur Technology. In David Hardin, editor, Design and Verification of
Microprocessor Systems for High-Assurance Applications, Pages 65-88.
Springer, 2010.
History
GL is the successor of Boyer and Hunt's G system, the best
description of which may be found in:
The name, GL, its name stands for G in the Logic. The G system was
written as a raw Lisp extension of the ACL2 kernel, so using it meant trusting
this additional code. In contrast, GL is implemented as ACL2 books and its
proof procedure is formally verified by ACL2, so the only code we have to trust
is in ACL2, including its hons-and-memoization features.
