Identify occurrences of basic, unsized parameters.
(vl-unsized-index-p x ss) → *
We often run into cases like
parameter foo = 5; ... assign w[3:0] = foo;
It was annoying to get truncation warnings about this sort of thing. So,
here, as a heuristic, we are looking for expression like
Function:
(defun vl-unsized-index-p (x ss) (declare (xargs :guard (and (vl-expr-p x) (vl-scopestack-p ss)))) (let ((__function__ 'vl-unsized-index-p)) (declare (ignorable __function__)) (vl-expr-case x :vl-index (b* (((when (or x.indices (not (vl-partselect-case x.part :none)))) nil) ((mv err trace ?context tail) (vl-follow-scopeexpr x.scope ss)) ((when err) nil) ((when (vl-hidexpr-case tail :dot)) nil) (item (vl-hidstep->item (car trace))) ((when (mbe :logic (vl-paramdecl-p item) :exec (eq (tag item) :vl-paramdecl))) (b* (((vl-paramdecl item))) (vl-paramtype-case item.type :vl-implicitvalueparam t :vl-typeparam nil :vl-explicitvalueparam (and (vl-datatype-resolved-p item.type.type) (b* (((mv err size) (vl-datatype-size item.type.type))) (and (not err) (equal size 32))))))) ((when (mbe :logic (vl-vardecl-p item) :exec (eq (tag item) :vl-vardecl))) (b* (((vl-vardecl item))) (vl-datatype-case item.type :vl-coretype (member item.type.name '(:vl-int :vl-integer)) :otherwise nil)))) nil) :otherwise nil)))
Theorem:
(defthm vl-unsized-index-p-of-vl-expr-fix-x (equal (vl-unsized-index-p (vl-expr-fix x) ss) (vl-unsized-index-p x ss)))
Theorem:
(defthm vl-unsized-index-p-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-unsized-index-p x ss) (vl-unsized-index-p x-equiv ss))) :rule-classes :congruence)
Theorem:
(defthm vl-unsized-index-p-of-vl-scopestack-fix-ss (equal (vl-unsized-index-p x (vl-scopestack-fix ss)) (vl-unsized-index-p x ss)))
Theorem:
(defthm vl-unsized-index-p-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-unsized-index-p x ss) (vl-unsized-index-p x ss-equiv))) :rule-classes :congruence)