Process a symbolic test vector and prepare it to be run.
(stv-process name stv cstv mod) → pstv
An STV must be processed before it can be run with stv-run. This processing can be expensive and involves several steps.
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.
(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))))
(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)