		Search-engine friendly clone of the ACL2 documentation.

Condcheck

Vl-interface-condcheck!

Signature
(vl-interface-condcheck! x) → warnings
Arguments: x — Guard (vl-interface-p x).
Returns: warnings — Type (vl-warningtree-p warnings).

Definitions and Theorems

Function: vl-interface-condcheck!

(defun vl-interface-condcheck! (x)
 (declare (xargs :guard (vl-interface-p x)))
 (let ((__function__ 'vl-interface-condcheck!))
  (declare (ignorable __function__))
  (b* (((vl-interface x) (vl-interface-fix x)))
    (b* ((warnings ((lambda (x)
                      (vl-importlist-condcheck x nil))
                    x.imports))
         (warnings1 (vl-portlist-condcheck! x.ports))
         (warnings (vl-warningtree-cons warnings1 warnings))
         (warnings1 ((lambda (x)
                       (vl-portdecllist-condcheck x nil))
                     x.portdecls))
         (warnings (vl-warningtree-cons warnings1 warnings))
         (warnings1 (vl-modportlist-condcheck! x.modports))
         (warnings (vl-warningtree-cons warnings1 warnings))
         (warnings1 ((lambda (x)
                       (vl-vardecllist-condcheck x nil))
                     x.vardecls))
         (warnings (vl-warningtree-cons warnings1 warnings))
         (warnings1 ((lambda (x)
                       (vl-paramdecllist-condcheck x nil))
                     x.paramdecls))
         (warnings (vl-warningtree-cons warnings1 warnings))
         (warnings1 (vl-fundecllist-condcheck! x.fundecls))
         (warnings (vl-warningtree-cons warnings1 warnings))
         (warnings1 (vl-taskdecllist-condcheck! x.taskdecls))
         (warnings (vl-warningtree-cons warnings1 warnings))
         (warnings1 ((lambda (x)
                       (vl-typedeflist-condcheck x nil))
                     x.typedefs))
         (warnings (vl-warningtree-cons warnings1 warnings))
         (warnings1 (vl-dpiimportlist-condcheck! x.dpiimports))
         (warnings (vl-warningtree-cons warnings1 warnings))
         (warnings1 (vl-dpiexportlist-condcheck! x.dpiexports))
         (warnings (vl-warningtree-cons warnings1 warnings))
         (warnings1 (vl-propertylist-condcheck! x.properties))
         (warnings (vl-warningtree-cons warnings1 warnings))
         (warnings1 (vl-sequencelist-condcheck! x.sequences))
         (warnings (vl-warningtree-cons warnings1 warnings))
         (warnings1 (vl-clkdecllist-condcheck! x.clkdecls))
         (warnings (vl-warningtree-cons warnings1 warnings))
         (warnings1 (vl-gclkdecllist-condcheck! x.gclkdecls))
         (warnings (vl-warningtree-cons warnings1 warnings))
         (warnings1
              (vl-defaultdisablelist-condcheck! x.defaultdisables))
         (warnings (vl-warningtree-cons warnings1 warnings))
         (warnings1 (vl-bindlist-condcheck! x.binds))
         (warnings (vl-warningtree-cons warnings1 warnings))
         (warnings1 (vl-classlist-condcheck! x.classes))
         (warnings (vl-warningtree-cons warnings1 warnings))
         (warnings1 (vl-elabtasklist-condcheck! x.elabtasks))
         (warnings (vl-warningtree-cons warnings1 warnings))
         (warnings1 (vl-modinstlist-condcheck! x.modinsts))
         (warnings (vl-warningtree-cons warnings1 warnings))
         (warnings1 (vl-assignlist-condcheck! x.assigns))
         (warnings (vl-warningtree-cons warnings1 warnings))
         (warnings1 (vl-aliaslist-condcheck! x.aliases))
         (warnings (vl-warningtree-cons warnings1 warnings))
         (warnings1 (vl-assertionlist-condcheck! x.assertions))
         (warnings (vl-warningtree-cons warnings1 warnings))
         (warnings1 (vl-cassertionlist-condcheck! x.cassertions))
         (warnings (vl-warningtree-cons warnings1 warnings))
         (warnings1 (vl-alwayslist-condcheck! x.alwayses))
         (warnings (vl-warningtree-cons warnings1 warnings))
         (warnings1 (vl-initiallist-condcheck! x.initials))
         (warnings (vl-warningtree-cons warnings1 warnings))
         (warnings1 (vl-finallist-condcheck! x.finals))
         (warnings (vl-warningtree-cons warnings1 warnings))
         (warnings1 (vl-genelementlist-condcheck! x.generates))
         (warnings (vl-warningtree-cons warnings1 warnings))
         (warnings1 (vl-genvarlist-condcheck! x.genvars))
         (warnings (vl-warningtree-cons warnings1 warnings))
         (warnings1 ((lambda (x) (vl-atts-condcheck x nil))
                     x.atts))
         (warnings (vl-warningtree-cons warnings1 warnings))
         (warnings1 (vl-maybe-parse-temps-condcheck! x.parse-temps))
         (warnings (vl-warningtree-cons warnings1 warnings)))
      warnings))))

Theorem: vl-warningtree-p-of-vl-interface-condcheck!

(defthm vl-warningtree-p-of-vl-interface-condcheck!
  (b* ((warnings (vl-interface-condcheck! x)))
    (vl-warningtree-p warnings))
  :rule-classes :rewrite)

Theorem: vl-interface-condcheck!-of-vl-interface-fix-x

(defthm vl-interface-condcheck!-of-vl-interface-fix-x
  (equal (vl-interface-condcheck! (vl-interface-fix x))
         (vl-interface-condcheck! x)))

Theorem: vl-interface-condcheck!-vl-interface-equiv-congruence-on-x

(defthm vl-interface-condcheck!-vl-interface-equiv-congruence-on-x
  (implies (vl-interface-equiv x x-equiv)
           (equal (vl-interface-condcheck! x)
                  (vl-interface-condcheck! x-equiv)))
  :rule-classes :congruence)