(vl-atom-welltyped-p x) determines if an atomic expression is well-typed.
For every integer atom (whether constant or weird), the finalwidth and finaltype must agree with the origwidth and origtype of the guts.
For every identifier atom, the finalwidth and finaltype may differ from the identifier's declaration. These differences allow us to implicitly represent the sign-extension or zero-extension of a wire, register, or variable. Informally, we also generally expect that the finalwidth should never be less than the declaration's width, and that the finaltype should be signed only if the declaration is signed. But to allow vl-expr-welltyped-p not to take a module as an argument, we actually do not check that these expectations hold.
For string atoms, per Section 3.6 we say that the finalwidth must be 8 times the string's length (which, interestingly, may be zero). We also say that the finaltype is unsigned.
For all other atoms, we insist that the finaltype and finalwidth are
Function:
(defun vl-atom-welltyped-p (x) (declare (xargs :guard (vl-expr-p x))) (declare (xargs :guard (vl-atom-p x))) (let ((__function__ 'vl-atom-welltyped-p)) (declare (ignorable __function__)) (b* (((vl-atom x) x) ((when (vl-fast-constint-p x.guts)) (b* (((vl-constint x.guts) x.guts)) (and (eq x.finaltype x.guts.origtype) (eql x.finalwidth x.guts.origwidth)))) ((when (vl-fast-weirdint-p x.guts)) (b* (((vl-weirdint x.guts) x.guts)) (and (eq x.finaltype x.guts.origtype) (eql x.finalwidth x.guts.origwidth)))) ((when (vl-fast-id-p x.guts)) (and x.finaltype (posp x.finalwidth))) ((when (vl-fast-hidpiece-p x.guts)) (and x.finaltype (posp x.finalwidth))) ((when (vl-fast-string-p x.guts)) (b* (((vl-string x.guts) x.guts)) (and (eq x.finaltype :vl-unsigned) (eql x.finalwidth (* 8 (length x.guts.value)))))) ((when (eq (tag x.guts) :vl-extint)) (and x.finaltype (posp x.finalwidth)))) (and (not x.finalwidth) (not x.finaltype)))))
Theorem:
(defthm booleanp-of-vl-atom-welltyped-p (b* ((welltyped-p (vl-atom-welltyped-p x))) (booleanp welltyped-p)) :rule-classes :type-prescription)
Theorem:
(defthm vl-atom-welltyped-p-of-vl-expr-fix-x (equal (vl-atom-welltyped-p (vl-expr-fix x)) (vl-atom-welltyped-p x)))
Theorem:
(defthm vl-atom-welltyped-p-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-atom-welltyped-p x) (vl-atom-welltyped-p x-equiv))) :rule-classes :congruence)