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

Always Procedures. Always procedures in checkers are similar to those in modules.
Note the following restriction: in always_ff procedures only nonblocking assign-
ments are allowed; blocking assignments are forbidden. We postpone examples of
their usage until Sect. 9.4 .

Final Procedure. final procedures in checkers are not different from final
procedures in modules (see Sect. 2.2.2 ). They are executed at the end of simulation.
Their main purpose is to print statistical information and to check the final state of
the simulation.
final procedures may contain everything that functions may contain. There-
fore, checker final procedures may only immediate assertions (including simple,
deferred observed and deferred final).

Example 9.12. We can add a final procedure to the checker request_granted
defined in Example 9.7 to check that at the end of simulation there is no outstanding
request. For simplicity, we assume that both req and gnt are Boolean, and that the
request remains asserted until granted.

checker request_granted(req, gnt,n=1,
event clk = $inferred_clock,
untyped rst = $inferred_disable);
default clocking @clk; endclocking
default disable iff rst;

a1: assert property (req |-> nexttime [n] gnt);

final begin
a2: assert (!rst -> gnt || !req) else
$warning("Outstanding request at the end of simulation");

end
endchecker : request_granted

t

It is possible to write an entire checker consisting only of the final procedure.
Its purpose would be to check the quiescent state at the end of simulation to verify
that there are no outstanding transactions, and that some important scenarios were
observed at least once.

9.2.3 Scoping Rules

Checkers may be declared at the top-level, i.e., in the scope of a compilation
unit. All the preceding checker examples in this chapter were top-level checkers.
Checkers may also be declared in other scopes: in modules, interfaces, programs,
generate blocks, packages, and in other checkers. The reason for declaring checkers
in smaller scopes is to make them local to these scopes, and to make the objects