		Search-engine friendly clone of the ACL2 documentation.

Syntax

Vl-nettypename-p

Representation of wire types.

Wires in Verilog can be given certain types. We represent these types using certain keyword symbols, whose names correspond to the possible types.

This is an ordinary defenum.

Function: vl-nettypename-p

(defun vl-nettypename-p (x)
  (declare (xargs :guard t))
  (or (eq x ':vl-wire)
      (eq x ':vl-tri)
      (eq x ':vl-supply0)
      (eq x ':vl-supply1)
      (eq x ':vl-triand)
      (eq x ':vl-trior)
      (eq x ':vl-tri0)
      (eq x ':vl-tri1)
      (eq x ':vl-trireg)
      (eq x ':vl-uwire)
      (eq x ':vl-wand)
      (eq x ':vl-wor)))

Theorem: type-when-vl-nettypename-p

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