• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
      • Mlib
        • Scopestack
        • Filtering-by-name
        • Vl-namefactory
        • Substitution
        • Allexprs
        • Hid-tools
        • Vl-consteval
        • Range-tools
        • Lvalexprs
        • Hierarchy
        • Finding-by-name
        • Expr-tools
        • Expr-slicing
        • Stripping-functions
        • Stmt-tools
        • Modnamespace
        • Vl-parse-expr-from-str
        • Welltyped
        • Reordering-by-name
        • Flat-warnings
        • Genblob
        • Expr-building
        • Datatype-tools
        • Syscalls
        • Relocate
        • Expr-cleaning
        • Namemangle
        • Caremask
        • 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-p
            • Vl-atomicportexpr->internalname
            • 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
          • Vl-directionlist
        • Lvalues
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Port-expressions

Vl-port-direction

Attempt to determine the direction for a port.

Signature

(vl-port-direction port scope warnings) 
  → 
(mv warnings maybe-dir)

Arguments

port — The port whose direction is being decided.
    Guard (vl-port-p port).

scope — The module or interface containing the port.
    Guard (vl-scope-p scope).

warnings — Ordinary warnings accumulator, may be extended with non-fatal warnings.
    Guard (vl-warninglist-p warnings).

Returns

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

maybe-dir — The direction for this port, or nil on failure.
    Type (vl-maybe-direction-p maybe-dir).

We attempt to determine the direction of this port and return it. We can fail if the port is not well-formed or if there is no port declaration corresponding to this port. In this case we return nil as the maybe-dir, and add a non-fatal warning describing the problem.

Non-fatal warnings can also be added if a complex port has conflicting directions, e.g., imagine a port such as .foo({bar,baz}), where bar is an input and baz is an output. We regard such a port as an inout, and add a warning that this case is very unusual.

Definitions and Theorems

Function: vl-port-direction

(defun vl-port-direction (port scope warnings)
 (declare (xargs :guard (and (vl-port-p port)
                             (vl-scope-p scope)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-port-direction))
  (declare (ignorable __function__))
  (b* ((port (vl-port-fix port))
       ((unless (vl-port-wellformed-p port))
        (mv (warn :type :vl-bad-port
                  :msg "~a0 is not well-formed."
                  :args (list port))
            nil))
       ((when (eq (tag port) :vl-interfaceport))
        (mv (ok) nil))
       (names (vl-port->internalnames port))
       ((mv successp warnings dirs)
        (vl-port-direction-aux names scope warnings port))
       ((unless successp) (mv (ok) nil))
       ((when (or (atom (cdr dirs))
                  (all-equalp :vl-input dirs)
                  (all-equalp :vl-output dirs)
                  (all-equalp :vl-inout dirs)))
        (mv (ok) (car dirs))))
   (mv
    (warn
     :type :vl-bad-port
     :msg
     "~a0 refers to ~&1, which do not all agree upon a ~
                      direction.  We do not support this. Directions: ~&2."
     :args (list port names (mergesort dirs)))
    nil))))

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

(defthm vl-warninglist-p-of-vl-port-direction.warnings
  (b* (((mv ?warnings ?maybe-dir)
        (vl-port-direction port scope warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-maybe-direction-p-of-vl-port-direction.maybe-dir

(defthm vl-maybe-direction-p-of-vl-port-direction.maybe-dir
  (b* (((mv ?warnings ?maybe-dir)
        (vl-port-direction port scope warnings)))
    (vl-maybe-direction-p maybe-dir))
  :rule-classes :rewrite)

Theorem: vl-direction-p-of-vl-port-direction

(defthm vl-direction-p-of-vl-port-direction
 (equal
   (vl-direction-p (mv-nth 1
                           (vl-port-direction port scope warnings)))
   (if (mv-nth 1
               (vl-port-direction port scope warnings))
       t
     nil)))

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

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

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

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

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

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

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

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

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

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

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

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

Subtopics

Vl-port-direction-aux