		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)