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,
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.
(defun vl-dpiprop-p (x)
(declare (xargs :guard t))
(or (eq x 'nil)
(eq x ':vl-dpi-pure)
(eq x ':vl-dpi-context)))
(implies (vl-dpiprop-p x)
(if (if (symbolp x)
(if (not (equal x 't))
(not (equal x 'nil))
(equal x 'nil)))