Vl FAQ - acl2/acl2 GitHub Wiki

Some FAQ's about VL and hardware verification in ACL2

##Introduction

Some FAQ's from using VL (see :xdoc topic "Vl"). General "authored" by people new to VL. Anyone should feel free to expand this list, and the VL maintainer(s) will consider bringing these notes into the official documentation as appropriate.

##Questions

Questions

• Coverage proof fails.

At some point GL was configured to use the wrong definition for unsigned-byte-p. Add the following:

(table acl2::structural-decomp-defs 'unsigned-byte-p 'unsigned-byte-p)

• What's a "single identifier" in an always block, as in the following fatal warning?

  Expected all left-hand sides to be single identifiers, but found q[6:0] <= d[6:0];

The indexes into q and d are throwing off VL. That can be fixed by making your assignment from q to d, as in:

```q <= d```

• How can I use stv-debug to debug one of many calls of stv-run inside a def-gl-thm?

There are three key observations to answering this question: (1) use with-local-state so you can call stv-debug, (2) get out of the context of a defthm so that you actually get the-live-state for with-local-state, and (3) use top-level so you can actually run the call of with-local-state. E.g.:

(top-level
 (b* ((circuit1-input1 3) ; relevant
      (circuit1-input2 4) ; relevant
      (circuit1-input3 0) ; irrelevant but need something
      (in-alist (circuit1-stv-autoins))
      (out-alist (stv-run (circuit1-stv)
                          in-alist))
      (circuit2-input1 (cdr (assoc 'circuit1-output1 out-alist)))
      (circuit2-input2 (cdr (assoc 'circuit1-output2 out-alist)))
      (in-alist2 (circuit2-stv-autoins))
      (out-alist2 (stv-run (circuit2-stv)
                           in-alist2))
      (circuit1-input3 (cdr (assoc 'circuit2-output1 out-alist2)))
      (in-alist3 (circuit1-stv-autoins))
      (out-alist3 (with-local-state
                   (mv-let
                     (out-alist3 state)
                     (stv-debug (circuit1-stv) ; stv-debug :)
                                in-alist3)
                     out-alist3)))
      (res (cdr (assoc 'circuit2-final-result out-alist3))))
   res))

Note that the above code is pseudo-code derived from code that actually worked, so I (Rager) can imagine that there are typos.

• Why won't my rewrite rule fire?

It may also be the case that your arguments to stv-run are in a different order in your lemma than in your checkpoint. We could fix this by having a version of std::defrule that canonicalized the order of inputs to stv-run, but that's work and makes std::defrule messy.