		Search-engine friendly clone of the ACL2 documentation.

Reasonable

Vl-module-check-reasonable

Annotate a module with any warnings concerning whether it is reasonable. Furthermore, if x is unreasonable, a fatal warning to it.

Signature
(vl-module-check-reasonable x) → new-x
Arguments: x — Guard (vl-module-p x).
Returns: new-x — Type (vl-module-p new-x), given the guard.

Definitions and Theorems

Function: vl-module-check-reasonable

(defun vl-module-check-reasonable (x)
  (declare (xargs :guard (vl-module-p x)))
  (let ((__function__ 'vl-module-check-reasonable))
    (declare (ignorable __function__))
    (b* (((when (vl-module->hands-offp x)) x)
         (warnings (vl-module->warnings x))
         ((mv okp warnings)
          (vl-module-reasonable-p-warn x warnings))
         (warnings (if okp (ok)
                     (fatal :type :vl-mod-unreasonable
                            :msg "Module ~m0 is unreasonable."
                            :args (list (vl-module->name x)))))
         (warnings (if (vl-module->generates x)
                       (fatal :type :vl-mod-has-generates
                              :msg "Module ~m0 has generate blocks."
                              :args (list (vl-module->name x)))
                     warnings))
         (x-prime (change-vl-module x
                                    :warnings warnings)))
      x-prime)))

Theorem: vl-module-p-of-vl-module-check-reasonable

(defthm vl-module-p-of-vl-module-check-reasonable
  (implies (and (force (vl-module-p x)))
           (b* ((new-x (vl-module-check-reasonable x)))
             (vl-module-p new-x)))
  :rule-classes :rewrite)