# 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.