		Search-engine friendly clone of the ACL2 documentation.

Svex-stvs

Svtv-debug-fsm

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

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

Definitions and Theorems

Function: svtv-debug-fsm-fn

(defun svtv-debug-fsm-fn (x inalists initst filename state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (svtv-p x)
                             (svex-envlist-p inalists)
                             (svex-env-p initst)
                             (stringp filename))))
 (let ((__function__ 'svtv-debug-fsm))
   (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-fsm-core x inalists initst
                          :filename filename))))

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

(defthm svtv-debug-fsm-fn-of-svtv-fix-x
  (equal (svtv-debug-fsm-fn (svtv-fix x)
                            inalists initst filename state)
         (svtv-debug-fsm-fn x inalists initst filename state)))

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

(defthm svtv-debug-fsm-fn-svtv-equiv-congruence-on-x
  (implies
       (svtv-equiv x x-equiv)
       (equal (svtv-debug-fsm-fn x inalists initst filename state)
              (svtv-debug-fsm-fn x-equiv
                                 inalists initst filename state)))
  :rule-classes :congruence)

Theorem: svtv-debug-fsm-fn-of-svex-envlist-fix-inalists

(defthm svtv-debug-fsm-fn-of-svex-envlist-fix-inalists
  (equal (svtv-debug-fsm-fn x (svex-envlist-fix inalists)
                            initst filename state)
         (svtv-debug-fsm-fn x inalists initst filename state)))

Theorem: svtv-debug-fsm-fn-svex-envlist-equiv-congruence-on-inalists

(defthm svtv-debug-fsm-fn-svex-envlist-equiv-congruence-on-inalists
 (implies
   (svex-envlist-equiv inalists inalists-equiv)
   (equal (svtv-debug-fsm-fn x inalists initst filename state)
          (svtv-debug-fsm-fn x
                             inalists-equiv initst filename state)))
 :rule-classes :congruence)

Theorem: svtv-debug-fsm-fn-of-svex-env-fix-initst

(defthm svtv-debug-fsm-fn-of-svex-env-fix-initst
  (equal (svtv-debug-fsm-fn x inalists (svex-env-fix initst)
                            filename state)
         (svtv-debug-fsm-fn x inalists initst filename state)))

Theorem: svtv-debug-fsm-fn-svex-env-equiv-congruence-on-initst

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

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

(defthm svtv-debug-fsm-fn-of-str-fix-filename
  (equal (svtv-debug-fsm-fn x inalists initst (str-fix filename)
                            state)
         (svtv-debug-fsm-fn x inalists initst filename state)))

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

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