How to do proofs about hardware models using STVs and FGL.
Part of the sv-tutorial. Previous section: stvs-and-testing.
The main engine for proofs about STVs is bitblasting. The suggested tool
for this is the
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
(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.
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
(and (unsigned-byte-p 16 b) (unsigned-byte-p 16 a) (unsigned-byte-p 3 op))
(list (cons 'A a) (cons 'B b) (cons 'OP op))
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:
To continue, next see decomposition-proofs.