• 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
          • Scopestack
          • Hid-tools
          • Filtering-by-name
          • Vl-interface-mocktype
          • Stripping-functions
          • Genblob
          • Expr-tools
          • Extract-vl-types
          • Hierarchy
          • Range-tools
          • Finding-by-name
          • Stmt-tools
          • Modnamespace
          • Flat-warnings
          • Reordering-by-name
          • Datatype-tools
          • Syscalls
          • Allexprs
          • Lvalues
          • Port-tools
            • Port-expressions
              • Vl-atomicportexprlist->internalnames
              • Vl-port-direction
              • Vl-portlist->internalnames
              • Vl-portexpr->internalnames
              • Vl-portdecls-with-dir
              • Vl-plainarglist-blankfree-p
              • Vl-namedarglist-blankfree-p
              • Vl-modinstlist-blankfree-p
              • Vl-ports-from-portdecls
              • Vl-portlist-wellformed-p
              • Vl-maybe-portexpr-p
              • Vl-portexpr-p
              • Vl-atomicportexpr->internalname
              • Vl-atomicportexpr-p
              • Vl-port->internalnames
                • Vl-atomicportexprlist-p
                • Vl-port-wellformed-p
                • Vl-plainarg-blankfree-p
                • Vl-namedarg-blankfree-p
                • Vl-modinst-blankfree-p
                • Vl-arguments-blankfree-p
          • Transforms
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Port-expressions

    Vl-port->internalnames

    Signature
    (vl-port->internalnames x) → names
    Arguments
    x — Guard (vl-port-p x).
    Returns
    names — Type (string-listp names).

    Definitions and Theorems

    Function: vl-port->internalnames

    (defun vl-port->internalnames (x)
      (declare (xargs :guard (vl-port-p x)))
      (declare (xargs :guard (vl-port-wellformed-p x)))
      (let ((__function__ 'vl-port->internalnames))
        (declare (ignorable __function__))
        (b* ((x (vl-port-fix x))
             ((when (eq (tag x) :vl-interfaceport))
              nil)
             (expr (vl-regularport->expr x))
             ((unless expr) nil))
          (vl-portexpr->internalnames expr))))

    Theorem: string-listp-of-vl-port->internalnames

    (defthm string-listp-of-vl-port->internalnames
      (b* ((names (vl-port->internalnames x)))
        (string-listp names))
      :rule-classes :rewrite)

    Theorem: vl-port->internalnames-of-vl-port-fix-x

    (defthm vl-port->internalnames-of-vl-port-fix-x
      (equal (vl-port->internalnames (vl-port-fix x))
             (vl-port->internalnames x)))

    Theorem: vl-port->internalnames-vl-port-equiv-congruence-on-x

    (defthm vl-port->internalnames-vl-port-equiv-congruence-on-x
      (implies (vl-port-equiv x x-equiv)
               (equal (vl-port->internalnames x)
                      (vl-port->internalnames x-equiv)))
      :rule-classes :congruence)