		Search-engine friendly clone of the ACL2 documentation.

Utilities

Vl-edition-p

Editions of the Verilog or SystemVerilog standards that VL attempts to implement.

Certain parts of VL are configurable and can try follow different versions of the standard. We currently have some support for:

:verilog-2005 corresponds to IEEE Std 1364-2005.
:system-verilog-2012 corresponds to IEEE Std 1800-2012.

This is an ordinary defenum.

Function: vl-edition-p

(defun vl-edition-p (x)
  (declare (xargs :guard t))
  (or (eq x ':verilog-2005)
      (eq x ':system-verilog-2012)))

Theorem: type-when-vl-edition-p

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

Subtopics

Vl-parse-edition: Getopt option parser for Verilog editions.