• 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-overlap-compatible-p

Definitions and Theorems

Function: vl-overlap-compatible-p

(defun vl-overlap-compatible-p (names x palist ialist)
 (declare
  (xargs
      :guard
      (and (string-listp names)
           (vl-module-p x)
           (equal palist
                  (vl-make-portdecl-alist (vl-module->portdecls x)))
           (equal ialist (vl-make-moditem-alist x))
           (subsetp-equal
                names
                (vl-portdecllist->names (vl-module->portdecls x)))
           (subsetp-equal names (vl-module->modnamespace x)))))
 (if (atom names)
     (progn$ (fast-alist-free ialist)
             (fast-alist-free palist)
             t)
   (and (vl-portdecl-and-moduleitem-compatible-p
             (vl-fast-find-portdecl (car names)
                                    (vl-module->portdecls x)
                                    palist)
             (vl-fast-find-moduleitem (car names)
                                      x ialist))
        (vl-overlap-compatible-p (cdr names)
                                 x palist ialist))))

Function: vl-overlap-compatible-p-warn

(defun vl-overlap-compatible-p-warn (names x palist ialist warnings)
 (declare
  (xargs
   :guard
   (and
      (and (string-listp names)
           (vl-module-p x)
           (equal palist
                  (vl-make-portdecl-alist (vl-module->portdecls x)))
           (equal ialist (vl-make-moditem-alist x))
           (subsetp-equal
                names
                (vl-portdecllist->names (vl-module->portdecls x)))
           (subsetp-equal names (vl-module->modnamespace x)))
      (vl-warninglist-p warnings)))
  (ignorable warnings))
 (if (atom names)
     (progn$ (fast-alist-free ialist)
             (fast-alist-free palist)
             (mv t warnings))
   (b*
    (((mv __ok1__ warnings)
      (vl-portdecl-and-moduleitem-compatible-p-warn
           (vl-fast-find-portdecl (car names)
                                  (vl-module->portdecls x)
                                  palist)
           (vl-fast-find-moduleitem (car names)
                                    x ialist)
           warnings))
     ((mv __ok2__ warnings)
      (b* (((mv __ok1__ warnings)
            (vl-overlap-compatible-p-warn (cdr names)
                                          x palist ialist warnings))
           ((mv __ok2__ warnings) (mv t warnings)))
        (mv (and __ok1__ __ok2__) warnings))))
    (mv (and __ok1__ __ok2__) warnings))))

Theorem: eliminate-vl-overlap-compatible-p-warn

(defthm eliminate-vl-overlap-compatible-p-warn
 (equal
  (mv-nth
      0
      (vl-overlap-compatible-p-warn names x palist ialist warnings))
  (vl-overlap-compatible-p names x palist ialist)))

Theorem: vl-warninglist-p-of-vl-overlap-compatible-p-warn

(defthm vl-warninglist-p-of-vl-overlap-compatible-p-warn
 (implies
  (force (vl-warninglist-p warnings))
  (vl-warninglist-p (mv-nth 1
                            (vl-overlap-compatible-p-warn
                                 names x palist ialist warnings)))))