Determine if a concatenation such as
(vl-spurious-concatenation-p arg ss) → spurious-p
In early implementations of vl-expr-clean-concats, we
looked for singleton concatenations like
Unfortunately, it's tricky to safely do this before sizing has been done.
For instance, if we replace
However, we found that we still wanted to carry out this reduction in places
where it is safe. For instance, it seems okay to do this in the special
cases of bit- and part-selects: these expressions are always unsigned and,
e.g., there is no difference between extending
As an additional tweak, which we wanted for a particular VL-Mangle project,
we now also permit
Function:
(defun vl-spurious-concatenation-p (arg ss) (declare (xargs :guard (and (vl-expr-p arg) (vl-scopestack-p ss)))) (let ((__function__ 'vl-spurious-concatenation-p)) (declare (ignorable __function__)) (if (vl-fast-atom-p arg) (b* ((guts (vl-atom->guts arg)) ((when (vl-fast-constint-p guts)) (equal (vl-constint->origtype guts) :vl-unsigned)) ((when (vl-fast-weirdint-p guts)) (equal (vl-weirdint->origtype guts) :vl-unsigned)) ((unless (vl-fast-id-p guts)) nil) (look (vl-scopestack-find-item (vl-id->name guts) ss)) ((unless (and look (eq (tag look) :vl-vardecl) (vl-simplevar-p look))) nil)) (not (vl-simplevar->signedp look))) (or (eq (vl-nonatom->op arg) :vl-bitselect) (eq (vl-nonatom->op arg) :vl-partselect-colon)))))
Theorem:
(defthm booleanp-of-vl-spurious-concatenation-p (b* ((spurious-p (vl-spurious-concatenation-p arg ss))) (booleanp spurious-p)) :rule-classes :type-prescription)
Theorem:
(defthm vl-spurious-concatenation-p-of-vl-expr-fix-arg (equal (vl-spurious-concatenation-p (vl-expr-fix arg) ss) (vl-spurious-concatenation-p arg ss)))
Theorem:
(defthm vl-spurious-concatenation-p-vl-expr-equiv-congruence-on-arg (implies (vl-expr-equiv arg arg-equiv) (equal (vl-spurious-concatenation-p arg ss) (vl-spurious-concatenation-p arg-equiv ss))) :rule-classes :congruence)
Theorem:
(defthm vl-spurious-concatenation-p-of-vl-scopestack-fix-ss (equal (vl-spurious-concatenation-p arg (vl-scopestack-fix ss)) (vl-spurious-concatenation-p arg ss)))
Theorem:
(defthm vl-spurious-concatenation-p-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-spurious-concatenation-p arg ss) (vl-spurious-concatenation-p arg ss-equiv))) :rule-classes :congruence)