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.
(defun vl-direction-p (x)
(declare (xargs :guard t))
(or (eq x ':vl-input)
(eq x ':vl-output)
(eq x ':vl-inout)))
(implies (vl-direction-p x)
(if (symbolp x)
(if (not (equal x 't))
(not (equal x 'nil))