		Search-engine friendly clone of the ACL2 documentation.

Symbolic-test-vectors

Stv-run-check-dontcares

Test that a given setting of the don't-care bits of an STV are indeed don't-cares under the given input alist.

Signature
(stv-run-check-dontcares pstv input-alist dontcare-env &key skip quiet) → out-alist
Arguments: pstv — The symbolic test vector to run.
Guard (processed-stv-p pstv).; input-alist — An alist that should typically bind at least some of the input simulation variables to natural numbers, or to the symbol X. Any inputs that aren't mentioned are implicitly bound to X.; dontcare-env — An alist that determines the setting of the don't-care inputs to test. This is fixed so that it binds variables only to T or F.; skip — Advanced option to avoid computing certain outputs; see below.; quiet — Suppress debugging output. By default, stv-run will print certain debugging information. This is generally convenient in def-gl-thm forms involving an stv-run, and will allow you to see nicely-formatted debugging info when counter-examples are found. But you can use :quiet t to suppress it.
Returns: out-alist — Alist binding user-level STV outputs to either natural numbers or X.

Useful for cases where an STV output is X, this can be used to prove a somewhat weaker theorem about a hardware module. This function tests that the evaluation of the non-skipped signals under the given input alist is the same when:

the s-expression variables not determined by the input alist are all set to false, and
they are instead set according to the dontcare-env.

It returns T if the two evaluations match and NIL if there is any difference.

If you prove (using GL) that this function always returns T under a given input alist, you have shown that any Boolean setting of the initial states, off-pipe inputs, etc., is irrelevant to the value produced under the given input alist (which presumably includes settings for various control bits specific to the instruction of interest). You can then prove, say, that the circuit meets its spec under a setting of all these don't-care bits to false, and this then implies that the circuit meets its spec under every Boolean setting of those bits.

Definitions and Theorems

Function: stv-run-check-dontcares-fn

(defun
 stv-run-check-dontcares-fn
 (pstv input-alist dontcare-env skip quiet)
 (declare (xargs :guard (processed-stv-p pstv)))
 (let
  ((__function__ 'stv-run-check-dontcares))
  (declare (ignorable __function__))
  (time$
   (b*
      (((mv sigs ?out-usersyms)
        (stv-run-collect-eval-signals pstv skip))
       (- (or quiet
              (cw "STV Raw Inputs: ~x0.~%" input-alist)))
       (ev-alist (stv-run-make-eval-env pstv input-alist)))
      (4v-sexpr-alist-check-independent sigs ev-alist dontcare-env))
   :msg "; stv-run-check-dontcares: ~st sec, ~sa bytes.~%"
   :mintime 1)))

Theorem: stv-run-check-dontcares-normalize-quiet

(defthm
  stv-run-check-dontcares-normalize-quiet
  (implies
       (syntaxp (not (equal quiet ''nil)))
       (equal (stv-run-check-dontcares pstv input-alist dontcare-env
                                       :skip skip
                                       :quiet quiet)
              (stv-run-check-dontcares pstv input-alist dontcare-env
                                       :skip skip))))