Stv-run
Evaluate a symbolic test vector at particular, concrete inputs.
- Signature
(stv-run 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.
Evaluating an stv basically involves three steps:
- We translate the input-alist into bit-level bindings; see stv-simvar-inputs-to-bits.
- Using these bit-level bindings, we evaluate the relevant output bits from
the processed STV, basically by calling 4v-sexpr-eval on each output
bit.
- We take the evaluated output bits and merge them back into a user-level
alist that binds the output simulation variables to natural numbers or Xes; see
stv-assemble-output-alist.
The optional skip argument may allow you to optimize this process,
especially in the context of gl proofs, when you don't care about the
values of certain output simulation variables. For instance, suppose you have
a module that emits several flags in addition to its result, but you don't care
about the flags for some instructions. Then, you can tell stv-run to skip
computing the flags as you verify these instructions, which may lead to a big
savings when BDDs are involved.
Definitions and Theorems
Function: stv-run-fn
(defun stv-run-fn (pstv input-alist skip quiet)
(declare (xargs :guard (processed-stv-p pstv)))
(let ((__function__ 'stv-run))
(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-simp-and-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: ~st sec, ~sa bytes.~%"
:mintime 1)))
Subtopics
- Stv-simvar-inputs-to-bits
- Convert the user-level input alist (which binds simulation variables
to naturals) into a bit-level alist for 4v-sexpr-eval.
- Stv-assemble-output-alist
- Convert the bit-level bindings from after 4v-sexpr-eval into
user-level bindings of the output simulation variables to naturals or X.
- Stv-print-alist
- Dumb printing utility. X is expected to be an alist binding symbols
to values. We print them out hexified and indented in a nice way.
