• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
        • Defwellformed
        • Reasonable
          • Vl-modulelist-check-reasonable
          • Vl-vardecl-reasonable-p
          • Vl-portdecl-and-moduleitem-compatible-p
          • Vl-module-reasonable-p
          • Vl-overlap-compatible-p
          • Vl-module-check-reasonable
          • Vl-portlist-reasonable-p
          • Vl-vardecllist-reasonable-p
          • Vl-modulelist-reasonable-p
        • Lvaluecheck
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Reasonable

Vl-module-reasonable-p

Definitions and Theorems

Function: vl-module-reasonable-p

(defun vl-module-reasonable-p (x)
  (declare (xargs :guard (vl-module-p x)))
  (b* (((vl-module x) x)
       (pdnames (vl-portdecllist->names x.portdecls))
       (pdnames-s (mergesort pdnames))
       (namespace (vl-module->modnamespace x))
       (namespace-s (mergesort namespace))
       (overlap (intersect pdnames-s namespace-s))
       (palist (vl-make-portdecl-alist x.portdecls))
       (ialist (vl-make-moditem-alist x)))
    (and (vl-portlist-reasonable-p x.ports)
         (vl-vardecllist-reasonable-p x.vardecls)
         t
         (if (mbe :logic (no-duplicatesp-equal namespace)
                  :exec (same-lengthp namespace namespace-s))
             t
           nil)
         (vl-overlap-compatible-p overlap x palist ialist))))

Function: vl-module-reasonable-p-warn

(defun vl-module-reasonable-p-warn (x warnings)
 (declare (xargs :guard (and (vl-module-p x)
                             (vl-warninglist-p warnings)))
          (ignorable warnings))
 (b* (((vl-module x) x)
      (pdnames (vl-portdecllist->names x.portdecls))
      (pdnames-s (mergesort pdnames))
      (namespace (vl-module->modnamespace x))
      (namespace-s (mergesort namespace))
      (overlap (intersect pdnames-s namespace-s))
      (palist (vl-make-portdecl-alist x.portdecls))
      (ialist (vl-make-moditem-alist x)))
  (b*
   (((mv __ok1__ warnings)
     (vl-portlist-reasonable-p-warn x.ports warnings))
    ((mv __ok2__ warnings)
     (b*
      (((mv __ok1__ warnings)
        (vl-vardecllist-reasonable-p-warn x.vardecls warnings))
       ((mv __ok2__ warnings)
        (b*
         (((mv __ok1__ warnings)
           (if (not x.initials)
               (mv t warnings)
            (mv
             t
             (cons
              (make-vl-warning
                 :type :vl-initial-stmts
                 :msg "~l0: module ~s1 contains initial statements."
                 :args (list x.minloc x.name))
              warnings))))
          ((mv __ok2__ warnings)
           (b*
            (((mv __ok1__ warnings)
              (if (mbe :logic (no-duplicatesp-equal namespace)
                       :exec (same-lengthp namespace namespace-s))
                  (mv t warnings)
               (mv
                nil
                (cons
                  (make-vl-warning
                       :type :vl-namespace-error
                       :msg "~l0: ~s1 illegally redefines ~&2."
                       :args
                       (list x.minloc
                             x.name (duplicated-members namespace)))
                  warnings))))
             ((mv __ok2__ warnings)
              (b* (((mv __ok1__ warnings)
                    (vl-overlap-compatible-p-warn
                         overlap x palist ialist warnings))
                   ((mv __ok2__ warnings) (mv t warnings)))
                (mv (and __ok1__ __ok2__) warnings))))
            (mv (and __ok1__ __ok2__) warnings))))
         (mv (and __ok1__ __ok2__) warnings))))
      (mv (and __ok1__ __ok2__) warnings))))
   (mv (and __ok1__ __ok2__) warnings))))

Theorem: eliminate-vl-module-reasonable-p-warn

(defthm eliminate-vl-module-reasonable-p-warn
  (equal (mv-nth 0
                 (vl-module-reasonable-p-warn x warnings))
         (vl-module-reasonable-p x)))

Theorem: vl-warninglist-p-of-vl-module-reasonable-p-warn

(defthm vl-warninglist-p-of-vl-module-reasonable-p-warn
  (implies (force (vl-warninglist-p warnings))
           (vl-warninglist-p
                (mv-nth 1
                        (vl-module-reasonable-p-warn x warnings)))))