|
|
|---|
|
|
|
|---|
GL modes allow you to control major aspects of how GL carries out its symbolic simulation and how it should solve Boolean formulas that arise during proofs.
For some general background, see section 4. Proving Theorems by Symbolic Execution of the basic-tutorial.
By default, GL operates in gl-bdd-mode. In this mode, the Boolean formulas within symbolic-objects are represented using ubdds, and questions about these formulas are resolved using BDD operations.
But GL also supports other modes, and you can easily switch between modes on a proof-by-proof basis. Typically this looks like:
(local (gl::gl-bdd-mode)) (def-gl-thm foo ...) (local (gl::gl-satlink-mode)) (def-gl-thm bar ...)
GL's other modes use And-Inverter Graphs (aigs) as the Boolean function representation. Unlike BDDs, AIGs are non-canonical, and this affects performance in fundamental ways: AIGs are generally much cheaper to construct than BDDs, but it can be hard to determine whether AIGs are equivalent, whereas with BDDs this is just a pointer-equality check.
A very convenient feature of AIGs is that you do not have to come up with a good variable ordering—this may be especially helpful on problems where case-splitting would be necessary because there's not a universally good BDD ordering. On the other hand, BDDs can provide especially nice counterexamples, whereas with AIGs we typically get just one, essentially random counterexample.
Performance-wise, AIGs are better for some problems and BDDs for others. Many operations combine bits from data buses in a regular, orderly way; in these cases, there is often a good BDD ordering and BDDs may be faster than our AIG modes. But when the operations are less regular, when no good BDD ordering is apparent, or when case-splitting seems necessary to get good BDD performance, the AIG modes may do better. For many of our proofs, AIG mode performs well and saves us the trouble of finding a good BDD ordering.
When AIGs are used to carry out GL proofs, we need some way to answer whether the final AIG is satisfiable. To do this, GL can use one of two back-end solvers.
Usually the better and higher-performance option is to send the AIG to an external SAT solver; see gl-satlink-mode. In this mode, GL uses the satlink library to call upon an off-the-shelf SAT solver. Using external SAT solvers raises questions of trust, and GL does not yet implement any sort of proof-checking for the SAT solver's output. But pragmatically, for most verification efforts, it is probably reasonable to trust a SAT solver.
Another option is to simply convert the AIG into BDDs; see gl-aig-bddify-mode. This isn't necessarily a good idea, and you still have to worry about the variable order in this case. Occasionally this may out-perform just using BDDs to begin with, because there are certain optimizations you can make when converting from AIGs to BDDs that aren't possible when you just use BDDs for everything. This is also a high-confidence mode, where the whole proof is carried out within ACL2, with just some minimal trust-tags to boost performance.