		Search-engine friendly clone of the ACL2 documentation.

Sv-tutorial

Proofs-with-stvs

How to do proofs about hardware models using STVs and FGL.

Part of the sv-tutorial. Previous section: stvs-and-testing.

FGL Setup

The main engine for proofs about STVs is bitblasting. The suggested tool for this is the FGL system. An alternative is the GL system, but this is no longer updated.

A prerequisite for effectively using FGL is to install a SAT solver. See satlink::sat-solver-options for instructions to install several SAT solvers. In particular, glucose is used in many of the community books (and this tutorial, by default), and Kissat is recommended for a high-performing general-purpose solver.

If you have installed glucose and have it in your PATH, the following FGL proofs should work with no further setup. Supposing you instead installed kissat and have that in your path, you could change the default solver used by FGL as follows. First define a 0-ary function with guard T that returns a satlink::config-p object:

(defun kissat-satlink-config
       nil (declare (xargs :guard t))
       (satlink::change-config satlink::*default-config*
                               :cmdline "kissat"))

Then attach that function to the stub fgl::fgl-satlink-config using defattach:

(defattach fgl::fgl-satlink-config
           kissat-satlink-config)

This lets FGL use Kissat as its default solver.

Once we have set up a SAT solver for FGL, we are ready to prove theorems with it. There are many more options for how to solve SAT problems with FGL; see fgl::fgl-solving for more.

Simple STV Proofs

Now that we've set up a symbolic test vector (in the previous section) and a SAT solver, we can try some proofs about it. Here is a simple example:

(fgl::def-fgl-thm
    alu16-adds
    :hyp (and (alu-test-vector-autohyps)
              (equal op *op-plus*))
    :concl (equal (cdr (assoc 'res
                              (svtv-run (alu-test-vector)
                                        (alu-test-vector-autoins))))
                  (loghead 16 (+ a b))))

In addition to defining the STV (alu-test-vector) itself, the defsvtv$ form from the previous section also defines the following macros/functions:

(alu-test-vector-autohyps) expands to a function that checks type hypotheses for the input variables -- in this case,

(and (unsigned-byte-p 16 b)
     (unsigned-byte-p 16 a)
     (unsigned-byte-p 3 op))

(alu-test-vector-autoins) expands to a function that takes the input variables as inputs and outputs an alist binding the variable symbols to their corresponding values, i.e.,

(list (cons 'A a)
      (cons 'B b)
      (cons 'OP op))

So the def-fgl-thm form above is checking that when the inputs a, b are appropriately-sized integers and op is set to the addition opcode, the res computed by the STV is (the low 16 bits of) the sum of a and b.

There are many ways to change the behavior of FGL and configure it to solve different sorts of problems. There is lots of documentation under fgl::fgl. Particular topics that might be of interest:

adding FGL rewrite rules
configuring SAT solving
using AIG transformations before SAT solving.

To continue, next see decomposition-proofs.