(svtv-debug-fsm-core x inalists initst &key (filename '"svtv-debug.vcd") (moddb 'moddb) (aliases 'aliases) (debugdata 'debugdata) (vcd-wiremap 'vcd-wiremap) (vcd-vals 'vcd-vals) (rewrite 't) (state 'state)) → (mv moddb aliases debugdata vcd-wiremap vcd-vals state)
Function:
(defun svtv-debug-fsm-core-fn (x inalists initst filename moddb aliases debugdata vcd-wiremap vcd-vals rewrite state) (declare (xargs :stobjs (moddb aliases debugdata vcd-wiremap vcd-vals state))) (declare (xargs :guard (and (svtv-p x) (svex-envlist-p inalists) (svex-env-p initst) (stringp filename)))) (let ((__function__ 'svtv-debug-fsm-core)) (declare (ignorable __function__)) (b* (((svtv x)) (mod-fn (intern-in-package-of-symbol (cat (symbol-name x.name) "-MOD") x.name)) ((mv err design) (magic-ev-fncall mod-fn nil state t t)) ((when err) (raise "Error: couldn't run ~x0: ~@1~%" mod-fn err) (mv moddb aliases debugdata vcd-wiremap vcd-vals state)) ((unless (and (design-p design) (modalist-addr-p (design->modalist design)))) (raise "Error: ~x0 returned a malformed design~%" mod-fn) (mv moddb aliases debugdata vcd-wiremap vcd-vals state)) ((mv err moddb aliases debugdata) (svtv-debug-init design)) ((when err) (mv moddb aliases debugdata vcd-wiremap vcd-vals state)) (debugdata (svtv-debug-set-svtv x :rewrite rewrite)) ((mv vcd-wiremap vcd-vals state) (svtv-debug-run-fsm inalists initst :filename filename))) (mv moddb aliases debugdata vcd-wiremap vcd-vals state))))
Theorem:
(defthm svtv-debug-fsm-core-fn-of-svtv-fix-x (equal (svtv-debug-fsm-core-fn (svtv-fix x) inalists initst filename moddb aliases debugdata vcd-wiremap vcd-vals rewrite state) (svtv-debug-fsm-core-fn x inalists initst filename moddb aliases debugdata vcd-wiremap vcd-vals rewrite state)))
Theorem:
(defthm svtv-debug-fsm-core-fn-svtv-equiv-congruence-on-x (implies (svtv-equiv x x-equiv) (equal (svtv-debug-fsm-core-fn x inalists initst filename moddb aliases debugdata vcd-wiremap vcd-vals rewrite state) (svtv-debug-fsm-core-fn x-equiv inalists initst filename moddb aliases debugdata vcd-wiremap vcd-vals rewrite state))) :rule-classes :congruence)
Theorem:
(defthm svtv-debug-fsm-core-fn-of-svex-envlist-fix-inalists (equal (svtv-debug-fsm-core-fn x (svex-envlist-fix inalists) initst filename moddb aliases debugdata vcd-wiremap vcd-vals rewrite state) (svtv-debug-fsm-core-fn x inalists initst filename moddb aliases debugdata vcd-wiremap vcd-vals rewrite state)))
Theorem:
(defthm svtv-debug-fsm-core-fn-svex-envlist-equiv-congruence-on-inalists (implies (svex-envlist-equiv inalists inalists-equiv) (equal (svtv-debug-fsm-core-fn x inalists initst filename moddb aliases debugdata vcd-wiremap vcd-vals rewrite state) (svtv-debug-fsm-core-fn x inalists-equiv initst filename moddb aliases debugdata vcd-wiremap vcd-vals rewrite state))) :rule-classes :congruence)
Theorem:
(defthm svtv-debug-fsm-core-fn-of-svex-env-fix-initst (equal (svtv-debug-fsm-core-fn x inalists (svex-env-fix initst) filename moddb aliases debugdata vcd-wiremap vcd-vals rewrite state) (svtv-debug-fsm-core-fn x inalists initst filename moddb aliases debugdata vcd-wiremap vcd-vals rewrite state)))
Theorem:
(defthm svtv-debug-fsm-core-fn-svex-env-equiv-congruence-on-initst (implies (svex-env-equiv initst initst-equiv) (equal (svtv-debug-fsm-core-fn x inalists initst filename moddb aliases debugdata vcd-wiremap vcd-vals rewrite state) (svtv-debug-fsm-core-fn x inalists initst-equiv filename moddb aliases debugdata vcd-wiremap vcd-vals rewrite state))) :rule-classes :congruence)
Theorem:
(defthm svtv-debug-fsm-core-fn-of-str-fix-filename (equal (svtv-debug-fsm-core-fn x inalists initst (str-fix filename) moddb aliases debugdata vcd-wiremap vcd-vals rewrite state) (svtv-debug-fsm-core-fn x inalists initst filename moddb aliases debugdata vcd-wiremap vcd-vals rewrite state)))
Theorem:
(defthm svtv-debug-fsm-core-fn-streqv-congruence-on-filename (implies (acl2::streqv filename filename-equiv) (equal (svtv-debug-fsm-core-fn x inalists initst filename moddb aliases debugdata vcd-wiremap vcd-vals rewrite state) (svtv-debug-fsm-core-fn x inalists initst filename-equiv moddb aliases debugdata vcd-wiremap vcd-vals rewrite state))) :rule-classes :congruence)