		Search-engine friendly clone of the ACL2 documentation.

Condcheck

Vl-design-condcheck!

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

Definitions and Theorems

Function: vl-design-condcheck!

(defun vl-design-condcheck! (x)
  (declare (xargs :guard (vl-design-p x)))
  (let ((__function__ 'vl-design-condcheck!))
    (declare (ignorable __function__))
    (b* (((vl-design x) (vl-design-fix x)))
      (b* ((warnings (vl-udplist-condcheck! x.udps))
           (warnings1 (vl-programlist-condcheck! x.programs))
           (warnings (vl-warningtree-cons warnings1 warnings))
           (warnings1 (vl-classlist-condcheck! x.classes))
           (warnings (vl-warningtree-cons warnings1 warnings))
           (warnings1 (vl-packagelist-condcheck! x.packages))
           (warnings (vl-warningtree-cons warnings1 warnings))
           (warnings1 (vl-configlist-condcheck! x.configs))
           (warnings (vl-warningtree-cons warnings1 warnings))
           (warnings1 ((lambda (x)
                         (vl-vardecllist-condcheck x nil))
                       x.vardecls))
           (warnings (vl-warningtree-cons warnings1 warnings))
           (warnings1 (vl-taskdecllist-condcheck! x.taskdecls))
           (warnings (vl-warningtree-cons warnings1 warnings))
           (warnings1 (vl-fundecllist-condcheck! x.fundecls))
           (warnings (vl-warningtree-cons warnings1 warnings))
           (warnings1 ((lambda (x)
                         (vl-paramdecllist-condcheck x nil))
                       x.paramdecls))
           (warnings (vl-warningtree-cons warnings1 warnings))
           (warnings1 ((lambda (x)
                         (vl-importlist-condcheck x nil))
                       x.imports))
           (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-fwdtypedeflist-condcheck! x.fwdtypes))
           (warnings (vl-warningtree-cons warnings1 warnings))
           (warnings1 ((lambda (x)
                         (vl-typedeflist-condcheck x nil))
                       x.typedefs))
           (warnings (vl-warningtree-cons warnings1 warnings))
           (warnings1 (vl-bindlist-condcheck! x.binds))
           (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)))
        warnings))))

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

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

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

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

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

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