• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
        • Syntax
        • Loader
        • Warnings
        • Getting-started
        • Utilities
        • Printer
        • Kit
        • Mlib
        • Transforms
          • Unparameterization
          • Elaborate
          • Addnames
          • Annotate
            • Increment-elim
            • Make-implicit-wires
            • Basic-bind-elim
            • Argresolve
              • Vl-convert-namedargs
              • Vl-unhierarchicalize-interfaceport
              • Vl-interfacelist-argresolve
              • Vl-modulelist-argresolve
              • Vl-gateinst-dirassign
              • Vl-arguments-argresolve
              • Vl-unhierarchicalize-interfaceports
              • Vl-check-blankargs
              • Vl-annotate-plainargs
              • Vl-modinst-maybe-argresolve
              • Vl-modinst-argresolve
              • Vl-modinstlist-argresolve
              • Vl-gateinstlist-dirassign
              • Vl-interface-argresolve
              • Vl-module-argresolve
              • Vl-namedarglist-alist
              • Vl-make-namedarg-alist
              • Vl-design-argresolve
              • Vl-fast-find-namedarg
              • Vl-namedarg-alist
              • Vl-scopeitem-modport-p
              • Vl-scopeitem-modinst-p
              • Vl-scopeitem-interfaceport-p
                • Vl-port-interface-p
              • Basicsanity
              • Portdecl-sign
              • Enum-names
              • Port-resolve
              • Udp-elim
              • Vl-annotate-design
              • Vl-annotate-module
            • Clean-warnings
            • Eliminitial
            • Custom-transform-hooks
            • Problem-modules
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Argresolve

    Vl-scopeitem-interfaceport-p

    Signature
    (vl-scopeitem-interfaceport-p x) → *
    Arguments
    x — Guard (vl-scopeitem-p x).

    Definitions and Theorems

    Function: vl-scopeitem-interfaceport-p$inline

    (defun vl-scopeitem-interfaceport-p$inline (x)
      (declare (xargs :guard (vl-scopeitem-p x)))
      (let ((__function__ 'vl-scopeitem-interfaceport-p))
        (declare (ignorable __function__))
        (mbe :logic (vl-interfaceport-p x)
             :exec (eq (tag x) :vl-interfaceport))))