		Search-engine friendly clone of the ACL2 documentation.

Svex-stvs

Svtv-debug

(Deprecated) Dump a VCD waveform showing the internal signals of an svex STV.

Signature
(svtv-debug x inalist &key (filename '"svtv-debug.vcd") (state 'state)) → state
Arguments: x — Guard (svtv-p x).; inalist — Guard (svex-env-p inalist).; filename — Guard (stringp filename).

This is deprecated in favor of svtv-debug$.

Definitions and Theorems

Function: svtv-debug-fn

(defun acl2::svtv-debug-fn (x inalist filename state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (svtv-p x)
                             (svex-env-p inalist)
                             (stringp filename))))
 (let ((__function__ 'svtv-debug))
   (declare (ignorable __function__))
   (b* (((acl2::local-stobjs moddb
                             aliases debugdata vcd-wiremap vcd-vals)
         (mv moddb aliases
             debugdata vcd-wiremap vcd-vals state)))
     (svtv-debug-core x inalist
                      :filename filename))))

Theorem: svtv-debug-fn-of-svtv-fix-x

(defthm acl2::svtv-debug-fn-of-svtv-fix-x
  (equal (acl2::svtv-debug-fn (svtv-fix x)
                              inalist filename state)
         (acl2::svtv-debug-fn x inalist filename state)))

Theorem: svtv-debug-fn-svtv-equiv-congruence-on-x

(defthm acl2::svtv-debug-fn-svtv-equiv-congruence-on-x
 (implies
   (svtv-equiv x acl2::x-equiv)
   (equal
        (acl2::svtv-debug-fn x inalist filename state)
        (acl2::svtv-debug-fn acl2::x-equiv inalist filename state)))
 :rule-classes :congruence)

Theorem: svtv-debug-fn-of-svex-env-fix-inalist

(defthm acl2::svtv-debug-fn-of-svex-env-fix-inalist
  (equal (acl2::svtv-debug-fn x (svex-env-fix inalist)
                              filename state)
         (acl2::svtv-debug-fn x inalist filename state)))

Theorem: svtv-debug-fn-svex-env-equiv-congruence-on-inalist

(defthm acl2::svtv-debug-fn-svex-env-equiv-congruence-on-inalist
 (implies
   (svex-env-equiv inalist acl2::inalist-equiv)
   (equal
        (acl2::svtv-debug-fn x inalist filename state)
        (acl2::svtv-debug-fn x acl2::inalist-equiv filename state)))
 :rule-classes :congruence)

Theorem: svtv-debug-fn-of-str-fix-filename

(defthm acl2::svtv-debug-fn-of-str-fix-filename
  (equal (acl2::svtv-debug-fn x inalist (str-fix filename)
                              state)
         (acl2::svtv-debug-fn x inalist filename state)))

Theorem: svtv-debug-fn-streqv-congruence-on-filename

(defthm acl2::svtv-debug-fn-streqv-congruence-on-filename
 (implies
   (acl2::streqv filename acl2::filename-equiv)
   (equal
        (acl2::svtv-debug-fn x inalist filename state)
        (acl2::svtv-debug-fn x inalist acl2::filename-equiv state)))
 :rule-classes :congruence)

Subtopics

Vcd.lisp
Debug.lisp