• 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-modulelist-reasonable-p

Definitions and Theorems

Function: vl-modulelist-reasonable-p

(defun vl-modulelist-reasonable-p (x)
  (declare (xargs :guard (vl-modulelist-p x)))
  (if (atom x)
      t
    (and (vl-module-reasonable-p (car x))
         (vl-modulelist-reasonable-p (cdr x)))))

Function: vl-modulelist-reasonable-p-warn

(defun vl-modulelist-reasonable-p-warn (x warnings)
  (declare (xargs :guard (and (vl-modulelist-p x)
                              (vl-warninglist-p warnings)))
           (ignorable warnings))
  (if (atom x)
      (mv t warnings)
    (b* (((mv __ok1__ warnings)
          (vl-module-reasonable-p-warn (car x)
                                       warnings))
         ((mv __ok2__ warnings)
          (b* (((mv __ok1__ warnings)
                (vl-modulelist-reasonable-p-warn (cdr x)
                                                 warnings))
               ((mv __ok2__ warnings) (mv t warnings)))
            (mv (and __ok1__ __ok2__) warnings))))
      (mv (and __ok1__ __ok2__) warnings))))

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

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

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

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