• 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-port-direction-aux
            • 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

• Vl-port-direction

Vl-port-direction-aux

Signature

(vl-port-direction-aux names scope warnings port) 
  → 
(mv successp warnings directions)

Arguments

names — Guard (string-listp names).

scope — Guard (vl-scope-p scope).

warnings — Guard (vl-warninglist-p warnings).

port — Guard (vl-port-p port).

Returns

successp — Type (booleanp successp).

warnings — Type (vl-warninglist-p warnings).

directions — Type (vl-directionlist-p directions).

Definitions and Theorems

Function: vl-port-direction-aux

(defun vl-port-direction-aux (names scope warnings port)
 (declare (xargs :guard (and (string-listp names)
                             (vl-scope-p scope)
                             (vl-warninglist-p warnings)
                             (vl-port-p port))))
 (let ((__function__ 'vl-port-direction-aux))
  (declare (ignorable __function__))
  (b* (((when (atom names)) (mv t (ok) nil))
       (name1 (string-fix (car names)))
       (decl (vl-scope-find-portdecl-fast name1 scope))
       ((mv successp warnings directions)
        (vl-port-direction-aux (cdr names)
                               scope warnings port))
       ((when decl)
        (mv successp warnings
            (cons (vl-portdecl->dir decl)
                  directions))))
   (mv
    nil
    (warn
     :type :vl-bad-port
     :msg
     "~a0 refers to ~w1, but there is no port declaration for ~
                      ~w1."
     :args (list (vl-port-fix port) name1))
    directions))))

Theorem: booleanp-of-vl-port-direction-aux.successp

(defthm booleanp-of-vl-port-direction-aux.successp
  (b* (((mv ?successp ?warnings ?directions)
        (vl-port-direction-aux names scope warnings port)))
    (booleanp successp))
  :rule-classes :type-prescription)

Theorem: vl-warninglist-p-of-vl-port-direction-aux.warnings

(defthm vl-warninglist-p-of-vl-port-direction-aux.warnings
  (b* (((mv ?successp ?warnings ?directions)
        (vl-port-direction-aux names scope warnings port)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-directionlist-p-of-vl-port-direction-aux.directions

(defthm vl-directionlist-p-of-vl-port-direction-aux.directions
  (b* (((mv ?successp ?warnings ?directions)
        (vl-port-direction-aux names scope warnings port)))
    (vl-directionlist-p directions))
  :rule-classes :rewrite)

Theorem: vl-port-direction-aux-mvtypes-2

(defthm vl-port-direction-aux-mvtypes-2
  (true-listp
       (mv-nth 2
               (vl-port-direction-aux names scope warnings port)))
  :rule-classes :type-prescription)

Theorem: vl-port-direction-aux-of-string-list-fix-names

(defthm vl-port-direction-aux-of-string-list-fix-names
  (equal (vl-port-direction-aux (string-list-fix names)
                                scope warnings port)
         (vl-port-direction-aux names scope warnings port)))

Theorem: vl-port-direction-aux-string-list-equiv-congruence-on-names

(defthm vl-port-direction-aux-string-list-equiv-congruence-on-names
 (implies
    (str::string-list-equiv names names-equiv)
    (equal (vl-port-direction-aux names scope warnings port)
           (vl-port-direction-aux names-equiv scope warnings port)))
 :rule-classes :congruence)

Theorem: vl-port-direction-aux-of-vl-scope-fix-scope

(defthm vl-port-direction-aux-of-vl-scope-fix-scope
  (equal (vl-port-direction-aux names (vl-scope-fix scope)
                                warnings port)
         (vl-port-direction-aux names scope warnings port)))

Theorem: vl-port-direction-aux-vl-scope-equiv-congruence-on-scope

(defthm vl-port-direction-aux-vl-scope-equiv-congruence-on-scope
 (implies
    (vl-scope-equiv scope scope-equiv)
    (equal (vl-port-direction-aux names scope warnings port)
           (vl-port-direction-aux names scope-equiv warnings port)))
 :rule-classes :congruence)

Theorem: vl-port-direction-aux-of-vl-warninglist-fix-warnings

(defthm vl-port-direction-aux-of-vl-warninglist-fix-warnings
  (equal (vl-port-direction-aux names
                                scope (vl-warninglist-fix warnings)
                                port)
         (vl-port-direction-aux names scope warnings port)))

Theorem: vl-port-direction-aux-vl-warninglist-equiv-congruence-on-warnings

(defthm
  vl-port-direction-aux-vl-warninglist-equiv-congruence-on-warnings
 (implies
    (vl-warninglist-equiv warnings warnings-equiv)
    (equal (vl-port-direction-aux names scope warnings port)
           (vl-port-direction-aux names scope warnings-equiv port)))
 :rule-classes :congruence)

Theorem: vl-port-direction-aux-of-vl-port-fix-port

(defthm vl-port-direction-aux-of-vl-port-fix-port
 (equal
     (vl-port-direction-aux names scope warnings (vl-port-fix port))
     (vl-port-direction-aux names scope warnings port)))

Theorem: vl-port-direction-aux-vl-port-equiv-congruence-on-port

(defthm vl-port-direction-aux-vl-port-equiv-congruence-on-port
 (implies
    (vl-port-equiv port port-equiv)
    (equal (vl-port-direction-aux names scope warnings port)
           (vl-port-direction-aux names scope warnings port-equiv)))
 :rule-classes :congruence)