		Search-engine friendly clone of the ACL2 documentation.

Vl-dpiimport

Vl-dpiprop-p

Representation of pure or context properties.

See SystemVerilog-2012 Sections 35.5.2 and 35.5.3. A DPI imported function (not task) can be declared as pure, which is supposed to be a promise that the C function's result only depends only on its inputs, doesn't do any file IO, doesn't access any global variables, etc.

Alternately, an imported function or task can be declared as context, which means that it is intended to call exported subroutines that access SystemVerilog data objects besides its arguments. The simulator may have to take special measures and avoid various optimizations when calling these functions.

This is an ordinary defenum.

Function: vl-dpiprop-p

(defun vl-dpiprop-p (x)
  (declare (xargs :guard t))
  (or (eq x 'nil)
      (eq x ':vl-dpi-pure)
      (eq x ':vl-dpi-context)))

Theorem: type-when-vl-dpiprop-p

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