		Search-engine friendly clone of the ACL2 documentation.

Stv-debug

Stv-make-snapshots

Prepare an STV for debugging by create "snapshots" that are ready to be evaluated and written to the VCD file.

Signature
(stv-make-snapshots pstv mod) → snapshots
Arguments: pstv — Guard (processed-stv-p pstv).
Returns: snapshots — Type (cons-list-listp 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.

Definitions and Theorems

Function: stv-make-snapshots

(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)))))

Theorem: cons-list-listp-of-stv-make-snapshots

(defthm cons-list-listp-of-stv-make-snapshots
        (b* ((snapshots (stv-make-snapshots pstv mod)))
            (cons-list-listp snapshots))
        :rule-classes :rewrite)