• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
        • Syntax
        • Loader
        • Warnings
        • Getting-started
        • Utilities
        • Printer
        • Kit
          • Vl-lint
            • Vl-lintconfig-p
            • Condcheck
            • Lint-warning-suppression
              • Vl-mash-warning-strings
              • Vl-design-lint-ignoreall
              • Vl-design-suppress-lint-warnings
                • Vl-interfacelist-suppress-lint-warnings
                • Vl-programlist-suppress-lint-warnings
                • Vl-packagelist-suppress-lint-warnings
                • Vl-modulelist-suppress-lint-warnings
                • Vl-configlist-suppress-lint-warnings
                • Vl-classlist-suppress-lint-warnings
                • Vl-udplist-suppress-lint-warnings
                • Vl-program-suppress-lint-warnings
                • Vl-package-suppress-lint-warnings
                • Vl-interface-suppress-lint-warnings
                  • Vl-module-suppress-lint-warnings
                  • Vl-config-suppress-lint-warnings
                  • Vl-class-suppress-lint-warnings
                  • Vl-udp-suppress-lint-warnings
                • Vl-ctxelement-scan-for-ignore
                • Vl-modelement-scan-for-ignore
                • Vl-warninglist-lint-ignoreall
                • Vl-function-specialization-map-scan-for-ignore
                • Vl-portdecl-or-blockitem-list-scan-for-ignore
                • Vl-portdecl-or-blockitem-scan-for-ignore
                • Vl-maybe-delayoreventcontrol-scan-for-ignore
                • Vl-fundecl-scan-for-ignore
                • Vl-function-specialization-scan-for-ignore
                • Vl-taskdecl-scan-for-ignore
                • Vl-modport-portlist-scan-for-ignore
                • Vl-delayoreventcontrol-scan-for-ignore
                • Vl-repeateventcontrol-scan-for-ignore
                • Vl-lint-suppress-warnings-att-compare-default
                • Vl-clkdecl-scan-for-ignore
                • Vl-vardecllist-scan-for-ignore
                • Vl-typedeflist-scan-for-ignore
                • Vl-taskdecllist-scan-for-ignore
                • Vl-sequencelist-scan-for-ignore
                • Vl-propportlist-scan-for-ignore
                • Vl-propertylist-scan-for-ignore
                • Vl-portdecllist-scan-for-ignore
                • Vl-plainarglist-scan-for-ignore
                • Vl-paramtype-scan-for-ignore
                • Vl-paramdecllist-scan-for-ignore
                • Vl-namedarglist-scan-for-ignore
                • Vl-modport-port-scan-for-ignore
                • Vl-modinstlist-scan-for-ignore
                • Vl-maybe-gatedelay-scan-for-ignore
                • Vl-maybe-exprdist-scan-for-ignore
                • Vl-lint-scan-for-ignore
                • Vl-lint-atts-say-ignore
                • Vl-lint-attname-says-ignore
                • Vl-fundecllist-scan-for-ignore
                • Vl-exprdistlist-scan-for-ignore
                • Vl-defaultdisable-scan-for-ignore
                • Vl-clkassignlist-scan-for-ignore
                • Vl-class-scan-for-ignore
                • Vl-blockitemlist-scan-for-ignore
                • Vl-blockitem-scan-for-ignore
                • Vl-vardecl-scan-for-ignore
                • Vl-sequence-scan-for-ignore
                • Vl-repetition-scan-for-ignore
                • Vl-regularport-scan-for-ignore
                • Vl-propspec-scan-for-ignore
                • Vl-propport-scan-for-ignore
                • Vl-property-scan-for-ignore
                • Vl-portdecl-scan-for-ignore
                • Vl-modinst-scan-for-ignore
                • Vl-maybe-clkskew-scan-for-ignore
                • Vl-interfaceport-scan-for-ignore
                • Vl-importlist-scan-for-ignore
                • Vl-gateinst-scan-for-ignore
                • Vl-gatedelay-scan-for-ignore
                • Vl-eventcontrol-scan-for-ignore
                • Vl-dpiimport-scan-for-ignore
                • Vl-distlist-scan-for-ignore
                • Vl-distitem-scan-for-ignore
                • Vl-delaycontrol-scan-for-ignore
                • Vl-typedef-scan-for-ignore
                • Vl-plainarg-scan-for-ignore
                • Vl-paramdecl-scan-for-ignore
                • Vl-namedarg-scan-for-ignore
                • Vl-modport-scan-for-ignore
                • Vl-maybe-rhs-scan-for-ignore
                • Vl-letdecl-scan-for-ignore
                • Vl-initial-scan-for-ignore
                • Vl-gclkdecl-scan-for-ignore
                • Vl-fwdtypedef-scan-for-ignore
                • Vl-exprdist-scan-for-ignore
                • Vl-elabtask-scan-for-ignore
                • Vl-dpiexport-scan-for-ignore
                • Vl-covergroup-scan-for-ignore
                • Vl-context1-scan-for-ignore
                • Vl-clkassign-scan-for-ignore
                • Vl-assign-scan-for-ignore
                • Vl-arguments-scan-for-ignore
                • Vl-rhs-scan-for-ignore
                • Vl-import-scan-for-ignore
                • Vl-genvar-scan-for-ignore
                • Vl-final-scan-for-ignore
                • Vl-clkskew-scan-for-ignore
                • Vl-bind-scan-for-ignore
                • Vl-always-scan-for-ignore
                • Vl-alias-scan-for-ignore
                • Vl-mash-warning-string
                • Vl-lint-suppress-warnings
                • Vl-warning-type-mash
                • Vl-lint-ignore-att-p
                • Vl-lint-ignore-att-mash
              • Lucid
              • Lvaluecheck
              • Vl-interfacelist-alwaysstyle
              • Truncation-warnings
              • Vl-modulelist-alwaysstyle
              • Skip-detection
              • Vl-lint-report
              • Vl-lintresult
              • Vl::vl-design-sv-use-set
              • Oddexpr-check
              • Leftright-check
              • Duplicate-detect
              • Selfassigns
              • *vl-lint-help*
              • Arith-compare-check
              • Dupeinst-check
              • Qmarksize-check
              • Lint-whole-file-suppression
              • Run-vl-lint-main
              • Logicassign
              • Run-vl-lint
              • Vl-print-certain-warnings
              • Duperhs-check
              • Vl-lint-top
              • Sd-filter-problems
              • Vl-modulelist-add-svbad-warnings
              • Vl-module-add-svbad-warnings
              • Check-case
              • Vl-lint-extra-actions
              • Drop-lint-stubs
              • Vl-lint-print-warnings
              • Drop-user-submodules
              • Check-namespace
              • Vl-lintconfig-loadconfig
              • Vl-lint-design->svex-modalist-wrapper
              • Vl-delete-sd-problems-for-modnames-aux
              • Vl-collect-new-names-from-orignames
              • Vl-lint-print-all-warnings
              • Vl-design-remove-unnecessary-modules
              • Vl-delete-sd-problems-for-modnames
              • Vl-always-check-style
              • Vl-vardecllist-svbad-warnings
              • Vl-vardecl-svbad-warnings
              • Vl-reportcard-remove-suppressed
              • Vl-reportcard-keep-suppressed
              • Vl-alwayslist-check-style
              • Vl-remove-nameless-descriptions
              • Vl-lint-apply-quiet
              • Vl-warninglist-remove-suppressed
              • Vl-warninglist-keep-suppressed
              • Vl-print-eliminated-descs
              • Vl-module-alwaysstyle
              • Vl-jp-reportcard-aux
              • Vl-interface-alwaysstyle
              • Vl-design-alwaysstyle
              • Vl-jp-description-locations
              • Vl-jp-reportcard
              • Vl-pp-stringlist-lines
              • Vl-jp-design-locations
              • Vl-datatype-svbad-p
              • Unpacked-range-check
              • Sd-problem-major-p
              • Vl-alwaysstyle
            • Vl-server
            • Vl-gather
            • Vl-zip
            • Vl-main
            • Split-plusargs
            • Vl-shell
            • Vl-json
          • Mlib
          • Transforms
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Vl-design-suppress-lint-warnings

    Vl-interface-suppress-lint-warnings

    Signature
    (vl-interface-suppress-lint-warnings x) → new-x
    Arguments
    x — Guard (vl-interface-p x).
    Returns
    new-x — Type (vl-interface-p new-x).

    Definitions and Theorems

    Function: vl-interface-suppress-lint-warnings

    (defun vl-interface-suppress-lint-warnings (x)
      (declare (xargs :guard (vl-interface-p x)))
      (let ((__function__ 'vl-interface-suppress-lint-warnings))
        (declare (ignorable __function__))
        (change-vl-interface
             x
             :warnings
             (vl-lint-suppress-warnings (vl-interface->warnings x)))))

    Theorem: vl-interface-p-of-vl-interface-suppress-lint-warnings

    (defthm vl-interface-p-of-vl-interface-suppress-lint-warnings
      (b* ((new-x (vl-interface-suppress-lint-warnings x)))
        (vl-interface-p new-x))
      :rule-classes :rewrite)

    Theorem: vl-interface-suppress-lint-warnings-of-vl-interface-fix-x

    (defthm vl-interface-suppress-lint-warnings-of-vl-interface-fix-x
      (equal (vl-interface-suppress-lint-warnings (vl-interface-fix x))
             (vl-interface-suppress-lint-warnings x)))

    Theorem: vl-interface-suppress-lint-warnings-vl-interface-equiv-congruence-on-x

    (defthm
     vl-interface-suppress-lint-warnings-vl-interface-equiv-congruence-on-x
     (implies (vl-interface-equiv x x-equiv)
              (equal (vl-interface-suppress-lint-warnings x)
                     (vl-interface-suppress-lint-warnings x-equiv)))
     :rule-classes :congruence)