		Search-engine friendly clone of the ACL2 documentation.

Symbolic-test-vectors

Stv-run-for-all-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-for-all-dontcares pstv input-alist &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.; 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.

NOTE: This function is not always executable; read on for details.

This function evaluates an STV under the input alist, like stv-run. However, stv-run effectively binds to X all input and initial state variables not set by the input alist (the don't-cares). Thus, for each output, stv-run produces either

an integer giving the value of that output, signifying that the don't-cares do not effect that output
an X, signifying that for some bit of that output, either the don't-cares may effect the value, or the value is X independent of the don't-cares.

This function instead produces:

an integer giving the value of that output, signifying that the don't-cares do not effect that output as long as they are Boolean-valued
an X, signifying that for some bit of that output, either the don't-cares may effect the value even when they are restricted to Boolean values, or the value is X independent of the don't-cares.

This function cannot always be straightforwardly computed: it may sometimes require solving a SAT problem to show that all possible assignments of Boolean values to the don't-care bits produce the same value of the outputs. Rather than calling a SAT solver in the midst of computing this function, we instead compute the result when it is straightforward, and produce an error (by calling a non-executable function) when it isn't.

Even when this function does not execute, it may be possible to prove that its result (say) matches a spec function, by doing the following:

Prove that the desired property holds of stv-run-squash-dontcares
Prove that stv-run-check-dontcares holds of the inputs to this function, for all don't-care alists.

Definitions and Theorems

Function: stv-run-for-all-dontcares-fn

(defun stv-run-for-all-dontcares-fn (pstv input-alist skip quiet)
 (declare (xargs :guard (processed-stv-p pstv)))
 (let ((__function__ 'stv-run-for-all-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))
     ((with-fast ev-alist))
     (evaled-out-bits
          (time$ (make-fast-alist
                      (4v-sexpr-boolconst-eval-alist sigs ev-alist))
                 :mintime 1/2
                 :msg "; stv-run out-bits: ~st sec, ~sa bytes.~%"))
     (- (fast-alist-free ev-alist))
     (assembled-outs
       (time$
            (stv-assemble-output-alist evaled-out-bits out-usersyms)
            :mintime 1/2
            :msg "; stv-run outs: ~st sec, ~sa bytes.~%"))
     (- (fast-alist-free evaled-out-bits))
     (- (or quiet
            (progn$ (cw "~%STV Inputs:~%")
                    (stv-print-alist input-alist)
                    (cw "~%STV Outputs:~%")
                    (stv-print-alist assembled-outs)
                    (cw "~%")))))
    assembled-outs)
   :msg "; stv-run-for-all-dontcares: ~st sec, ~sa bytes.~%"
   :mintime 1)))

Theorem: stv-run-for-all-dontcares-when-independent

(defthm stv-run-for-all-dontcares-when-independent
  (implies (stv-run-independent-of-dontcares pstv input-alist skip)
           (equal (stv-run-for-all-dontcares pstv input-alist
                                             :skip skip
                                             :quiet quiet)
                  (stv-run-squash-dontcares pstv input-alist
                                            :skip skip
                                            :quiet quiet))))