		Search-engine friendly clone of the ACL2 documentation.

Vl-classify-extension-warning-hook

Vl-classify-extension-warning-default

Default heuristic for filtering extension warnings.

Signature
(vl-classify-extension-warning-default lhs-size x-selfsize x ss) → *
Arguments: lhs-size — Guard (natp lhs-size).; x-selfsize — Guard (natp x-selfsize).; x — Guard (vl-expr-p x).; ss — Guard (vl-scopestack-p ss).

We found that extension warnings were frequently triggered by things like assign {carry,sum} = a + b where the designer seems to explicitly intend to get the carry bit. We therefore only cause a minor warning if the right-hand side is composed only of additions. Later it turned out we need to permit selects, too. And later we decided to also add subtraction as a permitted operation.

Another kind of extension warning that is stupidly minor is when we just have assignments like assign foo[127:0] = 0;. We now do not even create a minor warning for assignments where the rhs is a constant.

Definitions and Theorems

Function: vl-classify-extension-warning-default

(defun vl-classify-extension-warning-default
       (lhs-size x-selfsize x ss)
 (declare (xargs :guard (and (natp lhs-size)
                             (natp x-selfsize)
                             (vl-expr-p x)
                             (vl-scopestack-p ss))))
 (declare (ignorable lhs-size x-selfsize ss))
 (declare (xargs :guard (> lhs-size x-selfsize)))
 (let ((__function__ 'vl-classify-extension-warning-default))
  (declare (ignorable __function__))
  (vl-expr-case
   x :vl-literal
   (vl-value-case x.val
                  :vl-extint nil
                  :vl-constint (cond (x.val.wasunsized nil)
                                     ((eql x.val.value 0) nil)
                                     (t :vl-warn-extension))
                  :otherwise :vl-warn-extension)
   :vl-concat
   (if (|VL-EXPR-IS-{'0, ...}-P| x)
       nil
     :vl-warn-extension)
   :vl-multiconcat
   (if (vl-expr-is-{n{0}}-p x)
       nil
     :vl-warn-extension)
   :otherwise
   (b*
    ((ops (vl-expr-ops x))
     (minorp
      (and
       (or (member-equal :vl-binary-plus ops)
           (member-equal :vl-binary-minus ops)
           (member-equal :vl-binary-times ops))
       (subsetp-equal
           ops
           '(:vl-binary-plus :vl-binary-minus
                             :vl-partselect-colon :vl-bitselect)))))
    (if minorp :vl-warn-extension-minor
      :vl-warn-extension)))))

Theorem: vl-classify-extension-warning-default-of-nfix-lhs-size

(defthm vl-classify-extension-warning-default-of-nfix-lhs-size
 (equal
  (vl-classify-extension-warning-default (nfix lhs-size)
                                         x-selfsize x ss)
  (vl-classify-extension-warning-default lhs-size x-selfsize x ss)))

Theorem: vl-classify-extension-warning-default-nat-equiv-congruence-on-lhs-size

(defthm
 vl-classify-extension-warning-default-nat-equiv-congruence-on-lhs-size
 (implies
  (acl2::nat-equiv lhs-size lhs-size-equiv)
  (equal
    (vl-classify-extension-warning-default lhs-size x-selfsize x ss)
    (vl-classify-extension-warning-default
         lhs-size-equiv x-selfsize x ss)))
 :rule-classes :congruence)

Theorem: vl-classify-extension-warning-default-of-nfix-x-selfsize

(defthm vl-classify-extension-warning-default-of-nfix-x-selfsize
 (equal
  (vl-classify-extension-warning-default lhs-size (nfix x-selfsize)
                                         x ss)
  (vl-classify-extension-warning-default lhs-size x-selfsize x ss)))

Theorem: vl-classify-extension-warning-default-nat-equiv-congruence-on-x-selfsize

(defthm
 vl-classify-extension-warning-default-nat-equiv-congruence-on-x-selfsize
 (implies
  (acl2::nat-equiv x-selfsize x-selfsize-equiv)
  (equal
    (vl-classify-extension-warning-default lhs-size x-selfsize x ss)
    (vl-classify-extension-warning-default
         lhs-size x-selfsize-equiv x ss)))
 :rule-classes :congruence)

Theorem: vl-classify-extension-warning-default-of-vl-expr-fix-x

(defthm vl-classify-extension-warning-default-of-vl-expr-fix-x
 (equal
  (vl-classify-extension-warning-default
       lhs-size x-selfsize (vl-expr-fix x)
       ss)
  (vl-classify-extension-warning-default lhs-size x-selfsize x ss)))

Theorem: vl-classify-extension-warning-default-vl-expr-equiv-congruence-on-x

(defthm
 vl-classify-extension-warning-default-vl-expr-equiv-congruence-on-x
 (implies
  (vl-expr-equiv x x-equiv)
  (equal
    (vl-classify-extension-warning-default lhs-size x-selfsize x ss)
    (vl-classify-extension-warning-default
         lhs-size x-selfsize x-equiv ss)))
 :rule-classes :congruence)

Theorem: vl-classify-extension-warning-default-of-vl-scopestack-fix-ss

(defthm
      vl-classify-extension-warning-default-of-vl-scopestack-fix-ss
 (equal
  (vl-classify-extension-warning-default
       lhs-size
       x-selfsize x (vl-scopestack-fix ss))
  (vl-classify-extension-warning-default lhs-size x-selfsize x ss)))

Theorem: vl-classify-extension-warning-default-vl-scopestack-equiv-congruence-on-ss

(defthm
 vl-classify-extension-warning-default-vl-scopestack-equiv-congruence-on-ss
 (implies
  (vl-scopestack-equiv ss ss-equiv)
  (equal
    (vl-classify-extension-warning-default lhs-size x-selfsize x ss)
    (vl-classify-extension-warning-default
         lhs-size x-selfsize x ss-equiv)))
 :rule-classes :congruence)