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

￿ Macro encapsulation over the checker such that it would automatically provide
some of the keywords, thus simplifying instantiation (e.g., Example 24.6 ). It may
also hide differences between checker , property , and module -based checkers.
￿ Validation of values of arguments used as elaboration-time constants at elabora-
tion time. Using conditional generate statements to test the constant arguments,
elaboration tasks can issue error messages at elaboration, rather than at a later
time during simulation (possibly many hours after the start of the compilation of
the design).

The checker instances should also be easily identifiable by synthesis and
formal tools, without the need of 'ifndef — 'endif enclosures around the checker
instances. It is then left up to the tool to specify whether checkers should or should
not be included in the process.

24.3 Examples of Typical Checker Kinds

We now examine examples of different forms of checkers, illustrating the various
characteristics and limitations.

24.3.1 Simple Combinational Checker

The combinational checker shown in the following example is defined in a let
declaration, which is then used in a deferred assertion. Notice the configuration
mechanism using 'ifdef SYNTHESIS for selecting a form that is suitable for
synthesis and formal tools.

Example 24.2. let -based checker (in a package)
let onehot0 (sig, reset = 1'b1) =
'ifdef SYNTHESIS
// Selected for synthesis or formal
!|reset || $onehot0(sig);
'else
// Selected for 4-valued simulation
|reset === 0 ||
($onehot0(sig) && !$isunknown(reset_n);
'endif

t

Such a checker can be instantiated in a module (program or interface), and
procedural scope as follows.

Example 24.3. let -based checker instantiation
module m( input logic [3:0] r1,
output logic [3:0] r2);
a1: assert final (onehot0(r1))