		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-is-compiler-directive-p

List of Verilog-2005 compiler directives.

This list is taken directly from Section 19. We do not support some of these, but we need to recognize all of them so that we can complain when we run into ones we don't support, etc.

Centaur Extension. We also add `centaur_define, which we treat exactly as `define.

This is an ordinary defenum.

Function: vl-is-compiler-directive-p

(defun vl-is-compiler-directive-p (x)
  (declare (xargs :guard t))
  (or (equal x '"begin_keywords")
      (equal x '"celldefine")
      (equal x '"default_nettype")
      (equal x '"define")
      (equal x '"else")
      (equal x '"elsif")
      (equal x '"end_keywords")
      (equal x '"endcelldefine")
      (equal x '"endif")
      (equal x '"ifdef")
      (equal x '"ifndef")
      (equal x '"include")
      (equal x '"line")
      (equal x '"nounconnected_drive")
      (equal x '"pragma")
      (equal x '"resetall")
      (equal x '"timescale")
      (equal x '"unconnected_drive")
      (equal x '"undef")
      (equal x '"centaur_define")))

Theorem: type-when-vl-is-compiler-directive-p

(defthm type-when-vl-is-compiler-directive-p
  (implies (vl-is-compiler-directive-p x)
           (stringp x))
  :rule-classes :compound-recognizer)