		Search-engine friendly clone of the ACL2 documentation.

Lint-warning-suppression

Vl-modelement-scan-for-ignore

Signature
(vl-modelement-scan-for-ignore x mwtype) → ignorep
Arguments: x — Guard (vl-modelement-p x).; mwtype — Guard (stringp mwtype).
Returns: ignorep — Type (booleanp ignorep).

Definitions and Theorems

Function: vl-modelement-scan-for-ignore

(defun vl-modelement-scan-for-ignore (x mwtype)
 (declare (xargs :guard (and (vl-modelement-p x)
                             (stringp mwtype))))
 (let ((__function__ 'vl-modelement-scan-for-ignore))
  (declare (ignorable __function__))
  (let ((x (vl-modelement-fix x)))
   (common-lisp::case (tag x)
    ((:vl-portdecl)
     (b* ((ignorep (vl-portdecl-scan-for-ignore x mwtype)))
       ignorep))
    ((:vl-assign)
     (b* ((ignorep (vl-assign-scan-for-ignore x mwtype)))
       ignorep))
    ((:vl-alias)
     (b* ((ignorep (vl-alias-scan-for-ignore x mwtype)))
       ignorep))
    ((:vl-vardecl)
     (b* ((ignorep (vl-vardecl-scan-for-ignore x mwtype)))
       ignorep))
    ((:vl-paramdecl)
     (b* ((ignorep (vl-paramdecl-scan-for-ignore x mwtype)))
       ignorep))
    ((:vl-fundecl)
     (b* ((ignorep (vl-fundecl-scan-for-ignore x mwtype)))
       ignorep))
    ((:vl-taskdecl)
     (b* ((ignorep (vl-taskdecl-scan-for-ignore x mwtype)))
       ignorep))
    ((:vl-modinst)
     (b* ((ignorep (vl-modinst-scan-for-ignore x mwtype)))
       ignorep))
    ((:vl-gateinst)
     (b* ((ignorep (vl-gateinst-scan-for-ignore x mwtype)))
       ignorep))
    ((:vl-always)
     (b* ((ignorep (vl-always-scan-for-ignore x mwtype)))
       ignorep))
    ((:vl-initial)
     (b* ((ignorep (vl-initial-scan-for-ignore x mwtype)))
       ignorep))
    ((:vl-final)
     (b* ((ignorep (vl-final-scan-for-ignore x mwtype)))
       ignorep))
    ((:vl-typedef)
     (b* ((ignorep (vl-typedef-scan-for-ignore x mwtype)))
       ignorep))
    ((:vl-import)
     (b* ((ignorep (vl-import-scan-for-ignore x mwtype)))
       ignorep))
    ((:vl-fwdtypedef)
     (b* ((ignorep (vl-fwdtypedef-scan-for-ignore x mwtype)))
       ignorep))
    ((:vl-modport)
     (b* ((ignorep (vl-modport-scan-for-ignore x mwtype)))
       ignorep))
    ((:vl-genvar)
     (b* ((ignorep (vl-genvar-scan-for-ignore x mwtype)))
       ignorep))
    ((:vl-assertion)
     (b* ((ignorep (vl-assertion-scan-for-ignore x mwtype)))
       ignorep))
    ((:vl-cassertion)
     (b* ((ignorep (vl-cassertion-scan-for-ignore x mwtype)))
       ignorep))
    ((:vl-property)
     (b* ((ignorep (vl-property-scan-for-ignore x mwtype)))
       ignorep))
    ((:vl-sequence)
     (b* ((ignorep (vl-sequence-scan-for-ignore x mwtype)))
       ignorep))
    ((:vl-clkdecl)
     (b* ((ignorep (vl-clkdecl-scan-for-ignore x mwtype)))
       ignorep))
    ((:vl-gclkdecl)
     (b* ((ignorep (vl-gclkdecl-scan-for-ignore x mwtype)))
       ignorep))
    ((:vl-defaultdisable)
     (b* ((ignorep (vl-defaultdisable-scan-for-ignore x mwtype)))
       ignorep))
    ((:vl-dpiimport)
     (b* ((ignorep (vl-dpiimport-scan-for-ignore x mwtype)))
       ignorep))
    ((:vl-dpiexport)
     (b* ((ignorep (vl-dpiexport-scan-for-ignore x mwtype)))
       ignorep))
    ((:vl-bind)
     (b* ((ignorep (vl-bind-scan-for-ignore x mwtype)))
       ignorep))
    ((:vl-class)
     (b* ((ignorep (vl-class-scan-for-ignore x mwtype)))
       ignorep))
    ((:vl-covergroup)
     (b* ((ignorep (vl-covergroup-scan-for-ignore x mwtype)))
       ignorep))
    ((:vl-elabtask)
     (b* ((ignorep (vl-elabtask-scan-for-ignore x mwtype)))
       ignorep))
    (otherwise (b* ((ignorep (vl-letdecl-scan-for-ignore x mwtype)))
                 ignorep))))))

Theorem: booleanp-of-vl-modelement-scan-for-ignore

(defthm booleanp-of-vl-modelement-scan-for-ignore
  (b* ((ignorep (vl-modelement-scan-for-ignore x mwtype)))
    (booleanp ignorep))
  :rule-classes :type-prescription)

Theorem: vl-modelement-scan-for-ignore-of-vl-modelement-fix-x

(defthm vl-modelement-scan-for-ignore-of-vl-modelement-fix-x
  (equal (vl-modelement-scan-for-ignore (vl-modelement-fix x)
                                        mwtype)
         (vl-modelement-scan-for-ignore x mwtype)))

Theorem: vl-modelement-scan-for-ignore-vl-modelement-equiv-congruence-on-x

(defthm
  vl-modelement-scan-for-ignore-vl-modelement-equiv-congruence-on-x
  (implies (vl-modelement-equiv x x-equiv)
           (equal (vl-modelement-scan-for-ignore x mwtype)
                  (vl-modelement-scan-for-ignore x-equiv mwtype)))
  :rule-classes :congruence)

Theorem: vl-modelement-scan-for-ignore-of-str-fix-mwtype

(defthm vl-modelement-scan-for-ignore-of-str-fix-mwtype
  (equal (vl-modelement-scan-for-ignore x (str-fix mwtype))
         (vl-modelement-scan-for-ignore x mwtype)))

Theorem: vl-modelement-scan-for-ignore-streqv-congruence-on-mwtype

(defthm vl-modelement-scan-for-ignore-streqv-congruence-on-mwtype
  (implies (streqv mwtype mwtype-equiv)
           (equal (vl-modelement-scan-for-ignore x mwtype)
                  (vl-modelement-scan-for-ignore x mwtype-equiv)))
  :rule-classes :congruence)