(elab-mod->vcd-wires n codeidx elab-mod) → wires
Function:
(defun elab-mod->vcd-wires (n codeidx elab-mod) (declare (xargs :stobjs (elab-mod))) (declare (xargs :guard (and (natp n) (natp codeidx)))) (declare (xargs :guard (<= n (elab-mod-nwires elab-mod)))) (let ((__function__ 'elab-mod->vcd-wires)) (declare (ignorable __function__)) (b* (((when (mbe :logic (zp (- (elab-mod-nwires elab-mod) (nfix n))) :exec (eql (elab-mod-nwires elab-mod) n))) nil) (x (elab-mod-wiretablei n elab-mod)) ((wire x) x) (vcdwire (make-vcd-wire :name (name->string x.name) :msb (if x.revp x.low-idx (+ -1 x.width x.low-idx)) :lsb (if x.revp (+ -1 x.width x.low-idx) x.low-idx) :code (vcd-index->codestr codeidx))) (- (and (equal (vcd-wire->code vcdwire) "") (cw "Created empty-named wire for wire ~s0~%" x.name)))) (cons vcdwire (elab-mod->vcd-wires (1+ (lnfix n)) (1+ (lnfix codeidx)) elab-mod)))))
Theorem:
(defthm vcd-wirelist-p-of-elab-mod->vcd-wires (b* ((wires (elab-mod->vcd-wires n codeidx elab-mod))) (vcd-wirelist-p wires)) :rule-classes :rewrite)
Theorem:
(defthm len-of-elab-mod->vcd-wires (equal (len (elab-mod->vcd-wires n codeidx elab-mod)) (nfix (- (elab-mod-nwires elab-mod) (nfix n)))))
Theorem:
(defthm elab-mod->vcd-wires-of-nfix-n (equal (elab-mod->vcd-wires (nfix n) codeidx elab-mod) (elab-mod->vcd-wires n codeidx elab-mod)))
Theorem:
(defthm elab-mod->vcd-wires-nat-equiv-congruence-on-n (implies (nat-equiv n n-equiv) (equal (elab-mod->vcd-wires n codeidx elab-mod) (elab-mod->vcd-wires n-equiv codeidx elab-mod))) :rule-classes :congruence)
Theorem:
(defthm elab-mod->vcd-wires-of-nfix-codeidx (equal (elab-mod->vcd-wires n (nfix codeidx) elab-mod) (elab-mod->vcd-wires n codeidx elab-mod)))
Theorem:
(defthm elab-mod->vcd-wires-nat-equiv-congruence-on-codeidx (implies (nat-equiv codeidx codeidx-equiv) (equal (elab-mod->vcd-wires n codeidx elab-mod) (elab-mod->vcd-wires n codeidx-equiv elab-mod))) :rule-classes :congruence)
Theorem:
(defthm elab-mod->vcd-wires-of-elab-mod$a-fix-elab-mod (equal (elab-mod->vcd-wires n codeidx (elab-mod$a-fix elab-mod)) (elab-mod->vcd-wires n codeidx elab-mod)))
Theorem:
(defthm elab-mod->vcd-wires-elab-mod$a-equiv-congruence-on-elab-mod (implies (elab-mod$a-equiv elab-mod elab-mod-equiv) (equal (elab-mod->vcd-wires n codeidx elab-mod) (elab-mod->vcd-wires n codeidx elab-mod-equiv))) :rule-classes :congruence)