Prepare an STV for debugging by create "snapshots" that are ready to be evaluated and written to the VCD file.
(stv-make-snapshots pstv mod) → snapshots
This is computationally expensive. We memoize it so that we only need to make the snapshots the first time you want to debug an STV. The same snapshots can then be reused across as many calls of stv-debug as you like.
(defun stv-make-snapshots (pstv mod) (declare (xargs :guard (processed-stv-p pstv))) (let ((__function__ 'stv-make-snapshots)) (declare (ignorable __function__)) (b* (((processed-stv pstv) pstv) ((compiled-stv cstv) pstv.compiled-stv) (nphases (nfix cstv.nphases)) ((unless (posp nphases)) (raise "STV has no phases?")) ((mv ?init-st-general in-alists-general ?nst-alists-general out-alists-general int-alists-general) (time$ (stv-fully-general-simulation-debug nphases mod cstv.override-bits) :msg "; stv debug simulation: ~st sec, ~sa bytes.~%" :mintime 1/2))) (with-fast-alist cstv.restrict-alist (time$ (stv-combine-into-snapshots (4v-sexpr-restrict-with-rw-alists in-alists-general cstv.restrict-alist) (4v-sexpr-restrict-with-rw-alists out-alists-general cstv.restrict-alist) (4v-sexpr-restrict-with-rw-alists int-alists-general cstv.restrict-alist)) :msg "; stv-debug general snapshots: ~st sec, ~sa bytes.~%" :mintime 1/2)))))
(defthm cons-list-listp-of-stv-make-snapshots (b* ((snapshots (stv-make-snapshots pstv mod))) (cons-list-listp snapshots)) :rule-classes :rewrite)