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

|->
(

s_eventually [1:18] ack && (ack_tag == tag)
and
!(ack && (ack_tag == tag))

);
endproperty
a: assert property (p);

t

Or even more simply as
property p;
logic [3:0] tag;
(req, tag = req_tag)
|->
strong (
!(ack && (ack_tag == tag)) ##1
##[1:18] ack && (ack_tag == tag)

);
endproperty
a: assert property (p);

t
An alternative that may be more efficient with formal verification tools is to
separate the two cases into two independent assertions.

Example 19.5.
property p1;
logic [3:0] tag;
(req, tag = req_tag)
|->
s_eventually [1:18] ack && (ack_tag == tag);
endproperty
property p2;
logic [3:0] tag;
@( posedge clk) (req, tag = req_tag)
|->
!(ack && (ack_tag == tag));
endproperty
a1: assert property (p1);
a2: assert property (p2);

t
Finally, what if the lower bound is greater than 1 clock cycle, e.g., 3? A possible
solution to eliminate the unwanted early arrivals is to use a bounded always operator
as follows:

Example 19.6.
property p;
logic [3:0] tag;
(req, tag = req_tag)
|->
( s_eventually [3:18] ack && (ack_tag == tag))
and
( s_always [1:2] !(ack && (ack_tag == tag)));