Debugging Assertions and Efficiency Considerations - SVA: The Power of Assertions in SystemVerilog - page 423

about the failure or success of the assertion. The number of possibilities is quite
large to describe it in all generality; therefore, we shall illustrate the process using
an example.
Suppose that we need to debug an assertion written according to the following
requirements: When req becomes asserted for one clock cycle it is associated with
a transaction id req_tag , the acknowledgment ack is also associated with a similar
id ack_tag that establishes correspondence with the request having the same id.
ack must arrive no later than 18 cycles after the req . Acknowledgments can arrive
out of the requesting order.
Let us assume that the assertion has the following form:

Example 19.1.
property p;
logic [3:0] tag;
@( posedge clk) (req, tag = req_tag)
|=>
s_eventually [1:18] ack && (ack_tag == tag);
endproperty
a: assert property (p);

t

Clock ticks occur at times 1, 3, 5, ::: . An unexpected failure happened for the
attempt starting at 105, ending at 141. That is, the failure occurred at the limit of 18
clock cycles after req was received. Is the failure genuine?
Making association between the failure and the sequence of values is laborious,
so we opt for instrumenting the assertion and the test bench.

Example 19.2.
default clocking ck @( posedge clk);
endclocking
initial begin // add to the test
$assertoff();
#104;
// start assertion just before
// the start time of failure
$asserton();
#2;
// stop assertion right after
// the failing attempt at time 105
$assertoff();
end

property p;
logic [3:0] tag;
(

req, tag = req_tag, // make sure it triggered
$display("[%t] req asserted, tag %0d", $time, tag)

)
|=>
s_eventually [1:18] ack && (ack_tag == tag);
endproperty
a: assert property (p);