• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • 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)