		Search-engine friendly clone of the ACL2 documentation.

Vl-enumbasetype-p

Vl-enumbasekind-p

Kinds of base types for enums.

Signature
(vl-enumbasekind-p x) → *

The SystemVerilog-2012 rules for enum_base_type are:

enum_base_type ::=
    integer_atom_type   [signing]
  | integer_vector_type [signing] [packed_dimension]
  | type_identifier               [packed_dimension]

A vl-enumbasetag-p corresponds to the main part of this, i.e., it is either:

A string, corresponding to the name of the type_identifier
A symbol like :vl-byte, corresponding to an integer_atom_type, or
A symbol like :vl-logic, corresponding to an integer_vector_type.

Per Section 6.19, the default type is int.

Definitions and Theorems

Function: vl-enumbasekind-p

(defun vl-enumbasekind-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'vl-enumbasekind-p))
    (declare (ignorable __function__))
    (or (stringp x)
        (eq x :vl-byte)
        (eq x :vl-shortint)
        (eq x :vl-int)
        (eq x :vl-longint)
        (eq x :vl-integer)
        (eq x :vl-time)
        (eq x :vl-bit)
        (eq x :vl-logic)
        (eq x :vl-reg))))