Get the range, if any, for a data type.
(vl-datatype-range x) → (mv warning range)
The datatype should be fully resolved, as in the output from vl-datatype-usertype-elim.
What exactly do we mean by the range of a datatype? Most data types can have multiple array dimensions. What we mean is the range of indices that are valid to apply directly to the data structure: that is, the range of the "first" array dimension. This means: the leftmost unpacked dimension if there are unpacked dimensions; otherwise the leftmost packed dimension, otherwise nil. When types are composed, e.g. by declaring a type to be another type with some additional dimensions, the additional dimensions go to the left. Examples:
typedef logic [3:0] nibble; typedef nibble [7:0] quadword [1:0]; typedef quadword cacheline [15:0];
These are equivalent to:
typedef logic [3:0] nibble; typedef logic [7:0] [3:0] quadword [1:0]; typedef logic [7:0] [3:0] cacheline [15:0] [1:0];
A tricky part here is that a variable declaration's datatype doesn't necessarily include all of the unpacked array dimensions. In the declaration of my_kbyte, the type of my_kbyte is dword but it has additional dimensions stored in the variable declaration itself. So we take as an extra argument the unpacked dimensions of the datatype. If there are any unpacked dimensions, then the first unpacked dimension is transformed into the range; otherwise, it's the first packed dimension (or the declared range of a net type).
Function:
(defun vl-datatype-range (x) (declare (xargs :guard (vl-datatype-p x))) (let ((__function__ 'vl-datatype-range)) (declare (ignorable __function__)) (b* (((fun (fail msg args)) (mv (make-vl-warning :type :vl-datatype-range-fail :msg msg :args args) nil)) ((fun (success range)) (mv nil range)) (x (vl-datatype-fix x)) (udims (vl-datatype->udims x)) ((when (consp udims)) (b* ((dim (vl-packeddimension-fix (car udims))) ((when (eq dim :vl-unsized-dimension)) (fail "Most significant dimension is unsized: ~a0" (list x)))) (success dim))) (pdims (vl-datatype->pdims x)) ((when (consp pdims)) (b* (((when (eq (car pdims) :vl-unsized-dimension)) (fail "Most significant dimension is unsized: ~a0" (list x)))) (success (car pdims))))) (success nil))))
Theorem:
(defthm return-type-of-vl-datatype-range.warning (b* (((mv common-lisp::?warning ?range) (vl-datatype-range x))) (iff (vl-warning-p warning) warning)) :rule-classes :rewrite)
Theorem:
(defthm vl-maybe-range-p-of-vl-datatype-range.range (b* (((mv common-lisp::?warning ?range) (vl-datatype-range x))) (vl-maybe-range-p range)) :rule-classes :rewrite)
Theorem:
(defthm vl-datatype-range-of-vl-datatype-fix-x (equal (vl-datatype-range (vl-datatype-fix x)) (vl-datatype-range x)))
Theorem:
(defthm vl-datatype-range-vl-datatype-equiv-congruence-on-x (implies (vl-datatype-equiv x x-equiv) (equal (vl-datatype-range x) (vl-datatype-range x-equiv))) :rule-classes :congruence)