		Search-engine friendly clone of the ACL2 documentation.

Syntax

Vl-direction-p

Direction for a port declaration (input, output, or inout).

Each port declaration (see vl-portdecl-p) includes a direction to indicate that the port is either an input, output, or inout. We represent these directions with the keyword :vl-input, :vl-output, and :vl-inout, respectively.

In our argresolve transformation, directions are also assigned to all arguments of gate instances and most arguments of module instances. See our vl-plainarg-p structures for more information.

This is an ordinary defenum.

Function: vl-direction-p

(defun vl-direction-p (x)
  (declare (xargs :guard t))
  (or (eq x ':vl-input)
      (eq x ':vl-output)
      (eq x ':vl-inout)))

Theorem: type-when-vl-direction-p

(defthm type-when-vl-direction-p
  (implies (vl-direction-p x)
           (if (symbolp x)
               (if (not (equal x 't))
                   (not (equal x 'nil))
                 'nil)
             'nil))
  :rule-classes :compound-recognizer)