		Search-engine friendly clone of the ACL2 documentation.

Symbolic-test-vectors

Stv-process

Process a symbolic test vector and prepare it to be run.

Signature
(stv-process name stv cstv mod) → pstv
Arguments: name — A name for this STV. Used by stv-debug.
Guard (symbolp name).; stv — The bundled up, original symbolic test vector description that the user wrote. This isn't actually used for anything, except that we stuff it into the resulting processed-stv, perhaps mainly for documentation?.
Guard (stvdata-p stv).; cstv — An already-compiled version of stv. We take this as an argument, rather than compiling it ourselves, mainly to parallelize the STV book building process.
Guard (compiled-stv-p cstv).; mod — The esim module that stv is being written for.
Guard (good-esim-modulep mod).
Returns: pstv — The fully processed, ready-to-run STV.
Type (equal (processed-stv-p pstv) (if pstv t nil)), given (and (force (symbolp name)) (force (compiled-stv-p cstv))).

An STV must be processed before it can be run with stv-run. This processing can be expensive and involves several steps.

The mod is symbolically simulated using a fully-general multi-phase esim simulation.
The relevant outputs are then extracted from this simulation and specialized as suggested by this particular stv.
These restricted outputs and other information is then saved into a processed-stv-p object that can be given to stv-run or stv-debug.

Note that there are many chances for memoization, e.g., if you have a lot of different symbolic test vectors that all target the same module, they can reuse the same esim simulation, so processing the first STV may be very expensive but processing subsequent STVs can be much cheaper.

Definitions and Theorems

Function: stv-process

(defun stv-process (name stv cstv mod)
 (declare (xargs :guard (and (symbolp name)
                             (stvdata-p stv)
                             (compiled-stv-p cstv)
                             (good-esim-modulep mod))))
 (let ((__function__ 'stv-process))
  (declare (ignorable __function__))
  (b*
   (((compiled-stv cstv) cstv)
    (need-internals (not (subsetp cstv.int-extract-alists '(nil))))
    ((mv ?init-st-general
         ?in-alists-general nst-alists-general
         out-alists-general int-alists-general)
     (if need-internals
      (time$
        (stv-fully-general-simulation-debug
             cstv.nphases mod cstv.override-bits)
        :msg "; stv-process debug simulation: ~st sec, ~sa bytes.~%"
        :mintime 1/2)
      (time$ (stv-fully-general-simulation-run
                  cstv.nphases mod cstv.override-bits)
             :msg "; stv-process simulation: ~st sec, ~sa bytes.~%"
             :mintime 1/2)))
    (relevant-signals-general
     (time$
      (let*
       ((acc nil)
        (acc (stv-extract-relevant-signals cstv.out-extract-alists
                                           out-alists-general acc))
        (acc
           (if need-internals
               (stv-extract-relevant-signals cstv.int-extract-alists
                                             int-alists-general acc)
             acc))
        (acc (stv-extract-relevant-signals cstv.nst-extract-alists
                                           nst-alists-general acc)))
       acc)
      :msg "; stv-process extraction: ~st sec, ~sa bytes.~%"
      :mintime 1/2))
    (relevant-signals-specialized
     (time$
      (with-fast-alist
           cstv.restrict-alist
           (4v-sexpr-restrict-with-rw-alist relevant-signals-general
                                            cstv.restrict-alist))
      :msg "; stv-process specialization: ~st sec, ~sa bytes.~%"
      :mintime 1/2)))
   (make-processed-stv
        :name name
        :user-stv stv
        :compiled-stv cstv
        :relevant-signals relevant-signals-specialized))))

Theorem: return-type-of-stv-process

(defthm return-type-of-stv-process
  (implies (and (force (symbolp name))
                (force (compiled-stv-p cstv)))
           (b* ((pstv (stv-process name stv cstv mod)))
             (equal (processed-stv-p pstv)
                    (if pstv t nil))))
  :rule-classes :rewrite)

Subtopics

Processed-stv-p: Representation of a processed STV.
Stv-fully-general-simulation-run: Run an n step, fully general simulation of a module.
Stv-fully-general-in-alists: Create the sexpr-alists to use as the inputs for each phase of fully general simulations of a module.
Stv-run-esim-debug
Stv-extract-relevant-signals: Pull out the fully general expressions for the signals that we care about, and bind them to the bit names of the simulation variables.
Stv-fully-general-st-alist: Create the sexpr-alist to use as the initial state for fully general simulations of a module.
Stv-run-esim