• 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-portexpr->internalnames

    Collect the names of any internal wires that are connected to a well-formed port and return them as a list of strings.

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

    We just collect the names of the internal wires that are connected to the port. For instance, in the following module,

    module mod (a, .b(foo), .c( {bar[2], baz[width-1:0] } )) ;
      ...
    endmodule

    the internalnames for the first port are ("a"), the second port to ("foo"), and for the third port to ("bar" "baz").

    Note that we omit any names that occur in index expressions, i.e., notice how we omit width in the third port.

    Definitions and Theorems

    Function: vl-portexpr->internalnames

    (defun vl-portexpr->internalnames (x)
      (declare (xargs :guard (vl-expr-p x)))
      (declare (xargs :guard (vl-portexpr-p x)))
      (let ((__function__ 'vl-portexpr->internalnames))
        (declare (ignorable __function__))
        (if (vl-atomicportexpr-p x)
            (list (vl-atomicportexpr->internalname x))
          (vl-atomicportexprlist->internalnames (vl-concat->parts x)))))

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

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

    Theorem: vl-portexpr->internalnames-of-vl-expr-fix-x

    (defthm vl-portexpr->internalnames-of-vl-expr-fix-x
      (equal (vl-portexpr->internalnames (vl-expr-fix x))
             (vl-portexpr->internalnames x)))

    Theorem: vl-portexpr->internalnames-vl-expr-equiv-congruence-on-x

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