		Search-engine friendly clone of the ACL2 documentation.

Hid-tools

Vl-datatype-remove-dim

Get the type of a variable of type x after an indexing operation is applied to it.

Signature
(vl-datatype-remove-dim x) → (mv err caveat-flag new-x dim)
Arguments: x — Guard (vl-datatype-p x).
Returns: err — Error message on failure.
Type (iff (vl-msg-p err) err).; caveat-flag — Indicates caveat about possible signedness ambiguities.; new-x — Datatype after indexing.
Type (implies (not err) (vl-datatype-p new-x)).; dim — Dimension removed from the datatype.
Type (implies (not err) (vl-dimension-p dim)).

The caveat flag returned identifies a case where implementations disagree on the signedness of the resulting type. This caveat occurs when we have packed dimensions on a usertype that is declared as signed. In this case, if we index into an object down to the usertype, NCV treats the resulting object as signed, but VCS treats it as unsigned. The SV spec seems to say NCV's interpretation is correct: from Sec. 7.4.1, Packed Arrays:

If a packed array is declared as signed, then the array viewed as a single vector shall be signed. The individual elements of the array are unsigned unless they are of a named type declared as signed. A partselect of a packed array shall be unsigned.

An example:

typedef logic signed [3:0] squad;

squad [3:0] b;
assign b = 16'hffff;

logic [7:0] btest;
assign btest = b[1];

In NCVerilog, btest has the value ff, indicating that b[1] is considered signed; in VCS, btest has the value 0f, indicating that b[1] is considered unsigned.

Definitions and Theorems

Function: vl-datatype-remove-dim

(defun vl-datatype-remove-dim (x)
 (declare (xargs :guard (vl-datatype-p x)))
 (declare (xargs :guard (vl-datatype-resolved-p x)))
 (let ((__function__ 'vl-datatype-remove-dim))
   (declare (ignorable __function__))
   (b*
    ((x (vl-maybe-usertype-resolve x))
     (udims (vl-datatype->udims x))
     ((when (consp udims))
      (mv nil nil
          (vl-datatype-update-udims (cdr udims) x)
          (car udims)))
     (pdims (vl-datatype->pdims x))
     ((when (consp pdims))
      (b*
       ((x (vl-datatype-set-unsigned x))
        ((when (or (vl-datatype-case x :vl-usertype)
                   (consp (cdr pdims))))
         (mv nil nil
             (vl-datatype-update-dims (cdr pdims)
                                      nil x)
             (car pdims)))
        (new-x (vl-datatype-update-dims nil nil x))
        ((mv & arithclass)
         (vl-datatype-arithclass new-x))
        (caveat-flag
             (vl-arithclass-equiv arithclass :vl-signed-int-class)))
       (mv nil caveat-flag new-x (car pdims))))
     ((unless (vl-datatype-packedp x))
      (mv (vmsg "Index applied to non-packed, non-array type ~a0"
                x)
          nil nil nil))
     ((mv err size) (vl-datatype-size x))
     ((when err) (mv err nil nil nil))
     ((unless (posp size))
      (mv (vmsg "Index applied to ~s0 packed type: ~a1"
                (if size "unsizeable" "zero-sized")
                x)
          nil nil nil))
     ((when (and (vl-datatype-case x :vl-coretype)
                 (eql size 1)))
      (mv (vmsg "Index applied to bit type ~a0" x)
          nil nil nil))
     (dim (vl-range->dimension
               (make-vl-range :msb (vl-make-index (1- size))
                              :lsb (vl-make-index 0)))))
    (mv nil
        nil *vl-plain-old-logic-type* dim))))

Theorem: return-type-of-vl-datatype-remove-dim.err

(defthm return-type-of-vl-datatype-remove-dim.err
  (b* (((mv ?err ?caveat-flag ?new-x ?dim)
        (vl-datatype-remove-dim x)))
    (iff (vl-msg-p err) err))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-datatype-remove-dim.new-x

(defthm return-type-of-vl-datatype-remove-dim.new-x
  (b* (((mv ?err ?caveat-flag ?new-x ?dim)
        (vl-datatype-remove-dim x)))
    (implies (not err)
             (vl-datatype-p new-x)))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-datatype-remove-dim.dim

(defthm return-type-of-vl-datatype-remove-dim.dim
  (b* (((mv ?err ?caveat-flag ?new-x ?dim)
        (vl-datatype-remove-dim x)))
    (implies (not err)
             (vl-dimension-p dim)))
  :rule-classes :rewrite)

Theorem: vl-datatype-resolved-p-of-remove-dim

(defthm vl-datatype-resolved-p-of-remove-dim
  (b* (((mv ?err ?caveat-flag ?new-x ?dim)
        (vl-datatype-remove-dim x)))
    (implies (and (not err)
                  (vl-datatype-resolved-p x))
             (vl-datatype-resolved-p new-x))))

Theorem: no-error-when-pdims

(defthm no-error-when-pdims
  (b* (((mv ?err ?caveat-flag ?new-x ?dim)
        (vl-datatype-remove-dim x)))
    (implies (consp (vl-datatype->pdims x))
             (not err))))

Theorem: no-error-when-udims

(defthm no-error-when-udims
  (b* (((mv ?err ?caveat-flag ?new-x ?dim)
        (vl-datatype-remove-dim x)))
    (implies (consp (vl-datatype->udims x))
             (not err))))

Theorem: vl-datatype-remove-dim-of-vl-datatype-fix-x

(defthm vl-datatype-remove-dim-of-vl-datatype-fix-x
  (equal (vl-datatype-remove-dim (vl-datatype-fix x))
         (vl-datatype-remove-dim x)))

Theorem: vl-datatype-remove-dim-vl-datatype-equiv-congruence-on-x

(defthm vl-datatype-remove-dim-vl-datatype-equiv-congruence-on-x
  (implies (vl-datatype-equiv x x-equiv)
           (equal (vl-datatype-remove-dim x)
                  (vl-datatype-remove-dim x-equiv)))
  :rule-classes :congruence)