SVA for handshake

Question

i am trying to write a SVA assertion for a handshake procedure.

In my searches I have found the following:

property p_handshake(clk,req,ack);
@(posedge clk)
req |=> !req [*1:max] ##0 ack;
endproperty
assert property(p_handshake(clock,valid,done));

However, my "done" signal is allowed to come many cycles after the valid cycle goes high. How do you make this statement ensure that "done" is asserted at any point after valid is asserted, without valid being deasserted?

Answer 1

$rose(req) |=> req[*1:$] ##0 ack;

$rose will start the assertion on the rising edge of req. [*1:$] means the left hand side must be true for a range of 1 to unlimited clocks. You could use [+] which is equivalent to [*1:$].

Some other styles of writing the checker would be:

$rose(req) |-> req[*1:$] ##1 (ack && req);
$rose(req) |-> ##1 req throughout ack[->1];

Answer 2

don't you also need an SVA to ensure that when valid $rose's, the done is not already asserted? If you do, then pls consider this SVA- $rose(valid) |-> ~done ##1 $stable(~done) [*949:950] ##[1:$] done;

The above requires done to be non-asserted for a period followed by assertion sometime in the future.