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

else $error("a1 failed"); //check input
always_comb begin
r2=r1;
a2: assert final (onehot0(.sig(r2)))
else $error("a2 failed"); //check output
end
endmodule

t

Note the following features:

￿ A macro definition SYNTHESIS selects between two forms of let, one suitable
for formal tools and synthesizable checkers, and the other one for four-valued
simulation. In the latter case, the assertion is enabled when reset is 1 , disabled
(success) when reset is 0 , and it is forced to fail when reset is x ,or z .
￿ Both positional ( a1 ) and named ( a2 ) argument association can be used.
￿ The system function $onehot0 could be used directly in the assertion, however,
it would not provide for a disabling condition.
￿The reset argument has a default actual argument 1'b1 , meaning that when the
actual is not provided in an instance, the resetting condition is false by default as
shown in both a1 and a2 .
￿ The assertion is in the deferred form, hence it filters out 0-width glitches on both
reset and sig actual arguments.
￿ The assertions can be instantiated in the module scope like a1 , or in a procedure
like a2 .
￿ The

disabling condition cannot be inferred in let instances. That is,

$inferred_disable may not be used as a default actual argument.

24.3.2 A Checker-Based Combinational Checker

Next we examine a more flexible combinational checker. We assume that the
convention is that default disable iff provides an active low reset.
Example 24.4. Combinational checker
typedef enum {ASSERT, ASSUME, NONE} assert_type;
typedef bit [15:0] cover_type;

checker onehot0
(sig,
assert_type usage_kind = ASSERT,
cover_type cover_level = 1,
reset = $inferred_disable,
string msg = "", synthesis = 'SYNTHESIS);

if (cover_level<16'b0 || cover_level>16'b11)
// check valid coverage selection
$error("Coverage level is invalid %d",
cover_level,