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

1 checker request_granted( sequence req, property gnt,
2 untyped n=1, string msg = "",
3 event clk = $inferred_clock,
4 untyped rst = $inferred_disable, truncate = $);
5 default clocking @clk; endclocking
6 default disable iff rst;
7 if ($isunbounded(truncate))
8 sequence ante;
9 req;
10 endsequence : ante
11 else if (truncate < 1)
12 $error("truncate value should be positive");
13 else
14 sequence ante;
15 req intersect 1[ * 1:truncate];
16 endsequence : ante
17 a1: assert property (ante |-> nexttime [n] gnt) else $error(msg);
18 endchecker : request_granted

Fig. 9.6 Optional antecedent truncation

9.2.2.2 Checker Procedures

A checker may contain the following structural procedures: initial , always_comb ,
always_latch , always_ff and final .

Initial Procedure. In checkers, initial procedures may contain assertions, let
declarations and a procedural event control statement @ . All other statements are
forbidden there. The only purpose of initial procedures in checkers is to enable
assertions that execute a single evaluation attempt starting at the first tick of their
leading clock.

Example 9.11. Write a checker verifying that reset rst is initially high, then
eventually goes low and remains low forever.

Solution:

checker simple_reset(rst);
initial
a1: assert property (@$global_clock rst[+] #=# always !rst);
endchecker : simple_reset

Discussion: We need to check only the first evaluation attempt of a1 , hence it should
be placed in the scope of an initial procedure. We do not wish to associate the
behavior of rst with any specific clock; therefore, we chose the global clock, the
fastest clock of the system, to control this assertion. See Exercise 9.5 for further
discussion. t