Checker Libraries - SVA: The Power of Assertions in SystemVerilog - page 542

24.2.1 Temporality

Many interesting checkers can be stated as unclocked Boolean expressions. Often
clock is not needed and the user may be interested in instantiating the checker in
procedures or design modules that do not have access to any clock. Such checkers
cannot use concurrent assertions because they would require a clocking event.
For this purpose, deferred assertions (Sect. 4.3 ) are the best candidates. When it
is required to verify behaviors that are synchronous to some clock, concurrent
assertions need to be used. They can be Boolean expressions evaluating each attempt
at a single clock tick or temporal properties evaluating their attempts over several
clock ticks.

24.2.2 Encapsulation

property -based encapsulation for temporal checkers, and let -based encapsulation
for combinational checkers are the simplest ones. They are easy to use, but they
allow no modeling code and can encompass only a single assertion. They are usually
part of relatively simple checker libraries. More complex checkers that may consist
of several assertions, modeling code, and coverage items need encapsulation in
module , interface or more importantly now in checker constructs.

24.2.3 Packaging

Packaging checker libraries as a series of files, one per checker, in a “library”
directory that is included automatically during compilation is the most typical usage.
This mechanism has been used with the various existing module -based checker
libraries. checker , property and let encapsulations allow for a more robust
use model by packaging them in the SystemVerilog package enclosure. In this
way, the appropriate library can be “imported” only where it is needed. Therefore,
even different checkers with the same names can be deployed in different parts of
the design. Of course, there is always the third possibility by accessing checker
definitions that are brought into the source code using the 'include directive.
However, this method provides the least flexibility and we do not consider it further.

24.2.4 Configurability

Global configuration is achieved best by macros, for example, to accomplish the
following: