		Search-engine friendly clone of the ACL2 documentation.

Vl-lint

Vl-always-check-style

Signature
(vl-always-check-style x warnings) → warnings
Arguments: x — Guard (vl-always-p x).; warnings — Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-always-check-style

(defun vl-always-check-style (x warnings)
 (declare (xargs :guard (and (vl-always-p x)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-always-check-style))
  (declare (ignorable __function__))
  (b*
   (((vl-always x))
    (warnings
     (if
      (vl-alwaystype-equiv x.type :vl-always)
      (warn
       :type :vl-warn-plain-always
       :msg
       "~a0: legacy style always block in use, instead of ~
                         always_comb, always_ff, or always_latch."
       :args (list x))
      (ok)))
    (warnings (if (vl-alwaystype-equiv x.type :vl-always-latch)
                  (warn :type :vl-warn-always-latch
                        :msg "~a0: always_latch block found."
                        :args (list x))
                (ok))))
   warnings)))

Theorem: vl-warninglist-p-of-vl-always-check-style

(defthm vl-warninglist-p-of-vl-always-check-style
  (b* ((warnings (vl-always-check-style x warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)