		Search-engine friendly clone of the ACL2 documentation.

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