• 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-wellformed-p

    Recognizer for ports whose expressions are well-formed.

    Signature
    (vl-port-wellformed-p x) → *
    Arguments
    x — Guard (vl-port-p x).

    Definitions and Theorems

    Function: vl-port-wellformed-p

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

    Theorem: vl-port-wellformed-p-of-vl-port-fix-x

    (defthm vl-port-wellformed-p-of-vl-port-fix-x
      (equal (vl-port-wellformed-p (vl-port-fix x))
             (vl-port-wellformed-p x)))

    Theorem: vl-port-wellformed-p-vl-port-equiv-congruence-on-x

    (defthm vl-port-wellformed-p-vl-port-equiv-congruence-on-x
      (implies (vl-port-equiv x x-equiv)
               (equal (vl-port-wellformed-p x)
                      (vl-port-wellformed-p x-equiv)))
      :rule-classes :congruence)