Checkers - SVA: The Power of Assertions in SystemVerilog - page 210

9.5.2 Returning Assertion Status from Checkers

It may be useful to synthesize assertion in the chip, for example, to detect their
violations during post-silicon verification. In this case the corresponding checkers
need to be synthesized on the chip like modules. This may be done by introducing
an output checker argument to capture the assertion status and to return it to the
module where this checker has been instantiated.

Example 9.30. This example, borrowed from the LRM [ 8 ] with minor modifi-
cations, describes instantiation of a checker verifying the mutual exclusiveness
condition in a module and passing the assertion result to a scan latch.

1 checker mutex (sig,
2 event clk = $inferred_clock,
3 untyped rst = $inferred_disable,
4 output bit failure = 1'b0);
5 default clocking @clk; endclocking
6 default disable iff rst;
7 a1: assert property ($onehot0(sig))
8 failure = 1'b0; else failure = 1'b1;
9 endchecker : mutex
10
11 module m( input wire bus, logic clock, reset);
12

logic res, scan;

...

13

mutex check_bus(bus, posedge clock, reset, res);

14

always @( posedge clock) scan <= res;

15

endmodule :m

16

Checker mutex contains a single assertion a1 (Line 7 ) verifying that in its
argument sig at most one bit is set to 1. Normally assertions have only the fail
action, but this assertion has both pass and fail actions to capture assertion success
and failure (Line 8 ). Checker output argument failure captures the assertion status.
This checker is instantiated in module m as check_bus (Line 14 ) and it checks
for mutual exclusion of the bits of bus on each riding edge of clock . The result is
assigned to res in the Reactive region. Then it is fed to scan (presumably a scan
latch) by the nonblocking assignment (Line 15 ). On each rising edge of clock the
bits of bus are checked for mutual exclusion and the result is assigned to res in
the Reactive region. Note that if clock is changed in the Active region, scan will
capture the value of res generated on the previous rising edge of clock . t

9.5.3 Writing Modular Checkers

A module representing a complex design block may be split into several simpler
modules representing the component blocks. In this case the higher level module
connects instances of the lower level modules. The information is provided to lower