(svtv-debug-run-fsm inalists initst &key (filename '"svtv-debug.vcd") (moddb 'moddb) (aliases 'aliases) (debugdata 'debugdata) (vcd-wiremap 'vcd-wiremap) (vcd-vals 'vcd-vals) (state 'state)) → (mv vcd-wiremap vcd-vals state)
Function:
(defun svtv-debug-run-fsm-fn (inalists initst filename moddb aliases debugdata vcd-wiremap vcd-vals state) (declare (xargs :stobjs (moddb aliases debugdata vcd-wiremap vcd-vals state))) (declare (xargs :guard (and (svex-envlist-p inalists) (svex-env-p initst) (stringp filename)))) (declare (xargs :guard (and (moddb-ok moddb) (< (debugdata->modidx debugdata) (moddb->nmods moddb)) (<= (moddb-mod-totalwires (debugdata->modidx debugdata) moddb) (aliass-length aliases))))) (let ((__function__ 'svtv-debug-run-fsm)) (declare (ignorable __function__)) (b* (((debugdata debugdata)) (states (svex-alist-keys debugdata.nextstates)) (vcd-wiremap (resize-vcdwires (aliass-length aliases) vcd-wiremap)) ((mv scope & vcd-wiremap) (vcd-moddb->scopes "top" debugdata.modidx 0 0 moddb vcd-wiremap)) ((mv date state) (oslib::date)) (p (vcd-print-header date scope nil)) (vcd-vals (resize-4vecs (vcdwires-length vcd-wiremap) vcd-vals)) (in-vars (hons-set-diff (svexlist-collect-vars (append (svex-alist-vals debugdata.updates) (svex-alist-vals debugdata.nextstates))) (append (svex-alist-keys debugdata.updates) states))) (ins (svtv-expand-lines debugdata.ins debugdata.nphases)) ((mv ovlines ?ovs) (svtv-lines->overrides debugdata.overrides 0)) ((mv vcd-vals p) (svtv-debug-fsm-writephases 0 debugdata.nphases inalists ins ovlines initst debugdata.updates debugdata.nextstates in-vars aliases vcd-wiremap vcd-vals p)) ((mv channel state) (open-output-channel (mbe :logic (str-fix filename) :exec filename) :character state)) ((unless channel) (raise "Couldn't write vcd file ~s0~%" filename) (mv vcd-wiremap vcd-vals state)) (state (princ$ (vl-printedlist->string p) channel state)) (state (close-output-channel channel state))) (mv vcd-wiremap vcd-vals state))))
Theorem:
(defthm svtv-debug-run-fsm-fn-of-svex-envlist-fix-inalists (equal (svtv-debug-run-fsm-fn (svex-envlist-fix inalists) initst filename moddb aliases debugdata vcd-wiremap vcd-vals state) (svtv-debug-run-fsm-fn inalists initst filename moddb aliases debugdata vcd-wiremap vcd-vals state)))
Theorem:
(defthm svtv-debug-run-fsm-fn-svex-envlist-equiv-congruence-on-inalists (implies (svex-envlist-equiv inalists inalists-equiv) (equal (svtv-debug-run-fsm-fn inalists initst filename moddb aliases debugdata vcd-wiremap vcd-vals state) (svtv-debug-run-fsm-fn inalists-equiv initst filename moddb aliases debugdata vcd-wiremap vcd-vals state))) :rule-classes :congruence)
Theorem:
(defthm svtv-debug-run-fsm-fn-of-svex-env-fix-initst (equal (svtv-debug-run-fsm-fn inalists (svex-env-fix initst) filename moddb aliases debugdata vcd-wiremap vcd-vals state) (svtv-debug-run-fsm-fn inalists initst filename moddb aliases debugdata vcd-wiremap vcd-vals state)))
Theorem:
(defthm svtv-debug-run-fsm-fn-svex-env-equiv-congruence-on-initst (implies (svex-env-equiv initst initst-equiv) (equal (svtv-debug-run-fsm-fn inalists initst filename moddb aliases debugdata vcd-wiremap vcd-vals state) (svtv-debug-run-fsm-fn inalists initst-equiv filename moddb aliases debugdata vcd-wiremap vcd-vals state))) :rule-classes :congruence)
Theorem:
(defthm svtv-debug-run-fsm-fn-of-str-fix-filename (equal (svtv-debug-run-fsm-fn inalists initst (str-fix filename) moddb aliases debugdata vcd-wiremap vcd-vals state) (svtv-debug-run-fsm-fn inalists initst filename moddb aliases debugdata vcd-wiremap vcd-vals state)))
Theorem:
(defthm svtv-debug-run-fsm-fn-streqv-congruence-on-filename (implies (acl2::streqv filename filename-equiv) (equal (svtv-debug-run-fsm-fn inalists initst filename moddb aliases debugdata vcd-wiremap vcd-vals state) (svtv-debug-run-fsm-fn inalists initst filename-equiv moddb aliases debugdata vcd-wiremap vcd-vals state))) :rule-classes :congruence)
Theorem:
(defthm svtv-debug-run-fsm-fn-of-moddb-fix-moddb (equal (svtv-debug-run-fsm-fn inalists initst filename (moddb-fix moddb) aliases debugdata vcd-wiremap vcd-vals state) (svtv-debug-run-fsm-fn inalists initst filename moddb aliases debugdata vcd-wiremap vcd-vals state)))
Theorem:
(defthm svtv-debug-run-fsm-fn-moddb-equiv-congruence-on-moddb (implies (moddb-equiv moddb moddb-equiv) (equal (svtv-debug-run-fsm-fn inalists initst filename moddb aliases debugdata vcd-wiremap vcd-vals state) (svtv-debug-run-fsm-fn inalists initst filename moddb-equiv aliases debugdata vcd-wiremap vcd-vals state))) :rule-classes :congruence)
Theorem:
(defthm svtv-debug-run-fsm-fn-of-lhslist-fix-aliases (equal (svtv-debug-run-fsm-fn inalists initst filename moddb (lhslist-fix aliases) debugdata vcd-wiremap vcd-vals state) (svtv-debug-run-fsm-fn inalists initst filename moddb aliases debugdata vcd-wiremap vcd-vals state)))
Theorem:
(defthm svtv-debug-run-fsm-fn-lhslist-equiv-congruence-on-aliases (implies (lhslist-equiv aliases aliases-equiv) (equal (svtv-debug-run-fsm-fn inalists initst filename moddb aliases debugdata vcd-wiremap vcd-vals state) (svtv-debug-run-fsm-fn inalists initst filename moddb aliases-equiv debugdata vcd-wiremap vcd-vals state))) :rule-classes :congruence)