Look up the range for a wire or variable declaration.
(vl-slow-find-net/reg-range name mod) → (mv successp maybe-range)
Function:
(defun vl-slow-find-net/reg-range (name mod) (declare (xargs :guard (and (stringp name) (vl-module-p mod)))) (let ((__function__ 'vl-slow-find-net/reg-range)) (declare (ignorable __function__)) (b* ((find (vl-find-vardecl name (vl-module->vardecls mod))) ((unless (and find (vl-simplevar-p find))) (mv nil nil))) (mv t (vl-simplevar->range find)))))
Theorem:
(defthm booleanp-of-vl-slow-find-net/reg-range.successp (b* (((mv ?successp ?maybe-range) (vl-slow-find-net/reg-range name mod))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-maybe-range-p-of-vl-slow-find-net/reg-range.maybe-range (b* (((mv ?successp ?maybe-range) (vl-slow-find-net/reg-range name mod))) (vl-maybe-range-p maybe-range)) :rule-classes :rewrite)
Theorem:
(defthm vl-range-p-of-vl-slow-find-net/reg-range (b* (((mv ?successp ?maybe-range) (vl-slow-find-net/reg-range name mod))) (equal (vl-range-p maybe-range) (if maybe-range t nil))) :rule-classes :rewrite)
Theorem:
(defthm vl-slow-find-net/reg-range-of-vl-module-fix-mod (equal (vl-slow-find-net/reg-range name (vl-module-fix mod)) (vl-slow-find-net/reg-range name mod)))
Theorem:
(defthm vl-slow-find-net/reg-range-vl-module-equiv-congruence-on-mod (implies (vl-module-equiv mod mod-equiv) (equal (vl-slow-find-net/reg-range name mod) (vl-slow-find-net/reg-range name mod-equiv))) :rule-classes :congruence)