Test that a given setting of the don't-care bits of an STV are indeed don't-cares under the given input alist.
(stv-run-check-dontcares pstv input-alist dontcare-env &key skip quiet) → out-alist
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:
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.
(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)))
(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))))