|
|
|---|
|
|
|
|---|
(svtv-debug-fsm-writephases cycle nphases-per-cycle inalists
ins ovlines prev-st updates next-states
invars aliases vcd-wiremap vcd-vals p)
→
(mv vcd-vals1 p1)Function:
(defun svtv-debug-fsm-writephases (cycle nphases-per-cycle inalists ins ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p) (declare (xargs :stobjs (aliases vcd-wiremap vcd-vals))) (declare (xargs :guard (and (natp cycle) (natp nphases-per-cycle) (svex-envlist-p inalists) (svtv-lines-p ins) (svtv-overridelines-p ovlines) (svex-env-p prev-st) (svex-alist-p updates) (svex-alist-p next-states) (svarlist-p invars) (vl-printedlist-p p)))) (declare (xargs :guard (and (<= (aliass-length aliases) (vcdwires-length vcd-wiremap)) (<= (vcdwires-length vcd-wiremap) (4vecs-length vcd-vals)) (<= (aliass-length aliases) (4vecs-length vcd-vals))))) (let ((__function__ 'svtv-debug-fsm-writephases)) (declare (ignorable __function__)) (b* ((cycle (lnfix cycle)) (nphases-per-cycle (lnfix nphases-per-cycle)) (phase (* cycle nphases-per-cycle)) ((when (atom inalists)) (mv vcd-vals (vcd-dump-delta (* 10 (lnfix phase)) nil vcd-vals vcd-wiremap p))) (inalist (car inalists)) ((with-fast inalist)) ((mv vcd-vals p next-st) (svtv-debug-writephases 0 nphases-per-cycle phase inalist ins ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p))) (svtv-debug-fsm-writephases (1+ cycle) nphases-per-cycle (cdr inalists) ins ovlines next-st updates next-states invars aliases vcd-wiremap vcd-vals p))))
Theorem:
(defthm vl-printedlist-p-of-svtv-debug-fsm-writephases.p1 (b* (((mv ?vcd-vals1 ?p1) (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p))) (vl-printedlist-p p1)) :rule-classes :rewrite)
Theorem:
(defthm svtv-debug-fsm-writephases-of-nfix-cycle (equal (svtv-debug-fsm-writephases (nfix cycle) nphases-per-cycle inalists ins ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p) (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p)))
Theorem:
(defthm svtv-debug-fsm-writephases-nat-equiv-congruence-on-cycle (implies (nat-equiv cycle cycle-equiv) (equal (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p) (svtv-debug-fsm-writephases cycle-equiv nphases-per-cycle inalists ins ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p))) :rule-classes :congruence)
Theorem:
(defthm svtv-debug-fsm-writephases-of-nfix-nphases-per-cycle (equal (svtv-debug-fsm-writephases cycle (nfix nphases-per-cycle) inalists ins ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p) (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p)))
Theorem:
(defthm svtv-debug-fsm-writephases-nat-equiv-congruence-on-nphases-per-cycle (implies (nat-equiv nphases-per-cycle nphases-per-cycle-equiv) (equal (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p) (svtv-debug-fsm-writephases cycle nphases-per-cycle-equiv inalists ins ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p))) :rule-classes :congruence)
Theorem:
(defthm svtv-debug-fsm-writephases-of-svex-envlist-fix-inalists (equal (svtv-debug-fsm-writephases cycle nphases-per-cycle (svex-envlist-fix inalists) ins ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p) (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p)))
Theorem:
(defthm svtv-debug-fsm-writephases-svex-envlist-equiv-congruence-on-inalists (implies (svex-envlist-equiv inalists inalists-equiv) (equal (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p) (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists-equiv ins ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p))) :rule-classes :congruence)
Theorem:
(defthm svtv-debug-fsm-writephases-of-svtv-lines-fix-ins (equal (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists (svtv-lines-fix ins) ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p) (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p)))
Theorem:
(defthm svtv-debug-fsm-writephases-svtv-lines-equiv-congruence-on-ins (implies (svtv-lines-equiv ins ins-equiv) (equal (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p) (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins-equiv ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p))) :rule-classes :congruence)
Theorem:
(defthm svtv-debug-fsm-writephases-of-svtv-overridelines-fix-ovlines (equal (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins (svtv-overridelines-fix ovlines) prev-st updates next-states invars aliases vcd-wiremap vcd-vals p) (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p)))
Theorem:
(defthm svtv-debug-fsm-writephases-svtv-overridelines-equiv-congruence-on-ovlines (implies (svtv-overridelines-equiv ovlines ovlines-equiv) (equal (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p) (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines-equiv prev-st updates next-states invars aliases vcd-wiremap vcd-vals p))) :rule-classes :congruence)
Theorem:
(defthm svtv-debug-fsm-writephases-of-svex-env-fix-prev-st (equal (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines (svex-env-fix prev-st) updates next-states invars aliases vcd-wiremap vcd-vals p) (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p)))
Theorem:
(defthm svtv-debug-fsm-writephases-svex-env-equiv-congruence-on-prev-st (implies (svex-env-equiv prev-st prev-st-equiv) (equal (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p) (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st-equiv updates next-states invars aliases vcd-wiremap vcd-vals p))) :rule-classes :congruence)
Theorem:
(defthm svtv-debug-fsm-writephases-of-svex-alist-fix-updates (equal (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st (svex-alist-fix updates) next-states invars aliases vcd-wiremap vcd-vals p) (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p)))
Theorem:
(defthm svtv-debug-fsm-writephases-svex-alist-equiv-congruence-on-updates (implies (svex-alist-equiv updates updates-equiv) (equal (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p) (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st updates-equiv next-states invars aliases vcd-wiremap vcd-vals p))) :rule-classes :congruence)
Theorem:
(defthm svtv-debug-fsm-writephases-of-svex-alist-fix-next-states (equal (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st updates (svex-alist-fix next-states) invars aliases vcd-wiremap vcd-vals p) (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p)))
Theorem:
(defthm svtv-debug-fsm-writephases-svex-alist-equiv-congruence-on-next-states (implies (svex-alist-equiv next-states next-states-equiv) (equal (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p) (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st updates next-states-equiv invars aliases vcd-wiremap vcd-vals p))) :rule-classes :congruence)
Theorem:
(defthm svtv-debug-fsm-writephases-of-svarlist-fix-invars (equal (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st updates next-states (svarlist-fix invars) aliases vcd-wiremap vcd-vals p) (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p)))
Theorem:
(defthm svtv-debug-fsm-writephases-svarlist-equiv-congruence-on-invars (implies (svarlist-equiv invars invars-equiv) (equal (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p) (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st updates next-states invars-equiv aliases vcd-wiremap vcd-vals p))) :rule-classes :congruence)
Theorem:
(defthm svtv-debug-fsm-writephases-of-lhslist-fix-aliases (equal (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st updates next-states invars (lhslist-fix aliases) vcd-wiremap vcd-vals p) (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p)))
Theorem:
(defthm svtv-debug-fsm-writephases-lhslist-equiv-congruence-on-aliases (implies (lhslist-equiv aliases aliases-equiv) (equal (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st updates next-states invars aliases vcd-wiremap vcd-vals p) (svtv-debug-fsm-writephases cycle nphases-per-cycle inalists ins ovlines prev-st updates next-states invars aliases-equiv vcd-wiremap vcd-vals p))) :rule-classes :congruence)