|
|
|---|
|
|
|
|---|
(svtv-debug-run-logic inalist
&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-logic-fn (inalist 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-env-p inalist) (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-logic)) (declare (ignorable __function__)) (b* (((debugdata debugdata)) (states (svex-alist-keys debugdata.nextstates)) (initst (pairlis$ states (replicate (len states) (4vec-x)))) (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))) ((with-fast inalist)) (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 (list inalist) 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-logic-fn-of-svex-env-fix-inalist (equal (svtv-debug-run-logic-fn (svex-env-fix inalist) filename moddb aliases debugdata vcd-wiremap vcd-vals state) (svtv-debug-run-logic-fn inalist filename moddb aliases debugdata vcd-wiremap vcd-vals state)))
Theorem:
(defthm svtv-debug-run-logic-fn-svex-env-equiv-congruence-on-inalist (implies (svex-env-equiv inalist inalist-equiv) (equal (svtv-debug-run-logic-fn inalist filename moddb aliases debugdata vcd-wiremap vcd-vals state) (svtv-debug-run-logic-fn inalist-equiv filename moddb aliases debugdata vcd-wiremap vcd-vals state))) :rule-classes :congruence)
Theorem:
(defthm svtv-debug-run-logic-fn-of-str-fix-filename (equal (svtv-debug-run-logic-fn inalist (str-fix filename) moddb aliases debugdata vcd-wiremap vcd-vals state) (svtv-debug-run-logic-fn inalist filename moddb aliases debugdata vcd-wiremap vcd-vals state)))
Theorem:
(defthm svtv-debug-run-logic-fn-streqv-congruence-on-filename (implies (acl2::streqv filename filename-equiv) (equal (svtv-debug-run-logic-fn inalist filename moddb aliases debugdata vcd-wiremap vcd-vals state) (svtv-debug-run-logic-fn inalist filename-equiv moddb aliases debugdata vcd-wiremap vcd-vals state))) :rule-classes :congruence)
Theorem:
(defthm svtv-debug-run-logic-fn-of-moddb-fix-moddb (equal (svtv-debug-run-logic-fn inalist filename (moddb-fix moddb) aliases debugdata vcd-wiremap vcd-vals state) (svtv-debug-run-logic-fn inalist filename moddb aliases debugdata vcd-wiremap vcd-vals state)))
Theorem:
(defthm svtv-debug-run-logic-fn-moddb-equiv-congruence-on-moddb (implies (moddb-equiv moddb moddb-equiv) (equal (svtv-debug-run-logic-fn inalist filename moddb aliases debugdata vcd-wiremap vcd-vals state) (svtv-debug-run-logic-fn inalist filename moddb-equiv aliases debugdata vcd-wiremap vcd-vals state))) :rule-classes :congruence)
Theorem:
(defthm svtv-debug-run-logic-fn-of-lhslist-fix-aliases (equal (svtv-debug-run-logic-fn inalist filename moddb (lhslist-fix aliases) debugdata vcd-wiremap vcd-vals state) (svtv-debug-run-logic-fn inalist filename moddb aliases debugdata vcd-wiremap vcd-vals state)))
Theorem:
(defthm svtv-debug-run-logic-fn-lhslist-equiv-congruence-on-aliases (implies (lhslist-equiv aliases aliases-equiv) (equal (svtv-debug-run-logic-fn inalist filename moddb aliases debugdata vcd-wiremap vcd-vals state) (svtv-debug-run-logic-fn inalist filename moddb aliases-equiv debugdata vcd-wiremap vcd-vals state))) :rule-classes :congruence)