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

out <= tmp[DEL - 2];
end
end
endmodule : trans
This module generates signal out from signal in by delaying it by several clock
cycles specified by the module parameter DEL . Note that the if statement in module
trans is a generate if (see Example 2.2 ).
The following checker eventually_granted verifies that each request is even-
tually granted:

checker eventually_granted( sequence req, property gnt,
event clk = $inferred_clock);
assert property (@clk req |=> s_eventually gnt);
endchecker : eventually_granted
We can bind this checker to module trans to verify that the high value of signal
in of module trans is eventually transmitted to its output out :
bind trans eventually_granted
check_in2out(in, out, posedge clock);
The bind statement specifies that checker eventually_granted is bound to
each instance of module m . It is equivalent to instantiating the checker at the end of
module trans :
module trans #(DEL=1) ( input logic clock, in,
output logic out);

...
eventually_granted check_in2out(in, out, posedge clock);
endmodule : trans
Checker eventually_granted is too general, as it does not check the exact tim-
ing. To make more specific checks, it is possible to use checker request_granted :
checker request_granted( sequence req, property gnt, int n=1,
event clk = $inferred_clock, untyped rst = $inferred_disable);
a1: assert property (@clk disable iff (rst)
req |-> nexttime [n] gnt);
endchecker : request_granted
This time we cannot bind the checker to all instances of module trans ,
since the specific delay values are different in each instance: we need to bind
request_granted with the delay value of 1 to module instances ta and tb , and
with the delay value of 2 to module instance tc :
bind trans: ta, tb request_granted
delay1(in, out,, posedge clock);
bind trans: tc request_granted
delay2(in, out, 2, posedge clock);

t