|
|
|---|
|
|
|
|---|
(svtv-debug-core x inalist
&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-core-fn (x inalist 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-env-p inalist) (stringp filename)))) (let ((__function__ 'svtv-debug-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-logic inalist :filename filename))) (mv moddb aliases debugdata vcd-wiremap vcd-vals state))))
Theorem:
(defthm svtv-debug-core-fn-of-svtv-fix-x (equal (svtv-debug-core-fn (svtv-fix x) inalist filename moddb aliases debugdata vcd-wiremap vcd-vals rewrite state) (svtv-debug-core-fn x inalist filename moddb aliases debugdata vcd-wiremap vcd-vals rewrite state)))
Theorem:
(defthm svtv-debug-core-fn-svtv-equiv-congruence-on-x (implies (svtv-equiv x x-equiv) (equal (svtv-debug-core-fn x inalist filename moddb aliases debugdata vcd-wiremap vcd-vals rewrite state) (svtv-debug-core-fn x-equiv inalist filename moddb aliases debugdata vcd-wiremap vcd-vals rewrite state))) :rule-classes :congruence)
Theorem:
(defthm svtv-debug-core-fn-of-svex-env-fix-inalist (equal (svtv-debug-core-fn x (svex-env-fix inalist) filename moddb aliases debugdata vcd-wiremap vcd-vals rewrite state) (svtv-debug-core-fn x inalist filename moddb aliases debugdata vcd-wiremap vcd-vals rewrite state)))
Theorem:
(defthm svtv-debug-core-fn-svex-env-equiv-congruence-on-inalist (implies (svex-env-equiv inalist inalist-equiv) (equal (svtv-debug-core-fn x inalist filename moddb aliases debugdata vcd-wiremap vcd-vals rewrite state) (svtv-debug-core-fn x inalist-equiv filename moddb aliases debugdata vcd-wiremap vcd-vals rewrite state))) :rule-classes :congruence)
Theorem:
(defthm svtv-debug-core-fn-of-str-fix-filename (equal (svtv-debug-core-fn x inalist (str-fix filename) moddb aliases debugdata vcd-wiremap vcd-vals rewrite state) (svtv-debug-core-fn x inalist filename moddb aliases debugdata vcd-wiremap vcd-vals rewrite state)))
Theorem:
(defthm svtv-debug-core-fn-streqv-congruence-on-filename (implies (acl2::streqv filename filename-equiv) (equal (svtv-debug-core-fn x inalist filename moddb aliases debugdata vcd-wiremap vcd-vals rewrite state) (svtv-debug-core-fn x inalist filename-equiv moddb aliases debugdata vcd-wiremap vcd-vals rewrite state))) :rule-classes :congruence)