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?

score 2 · Accepted Answer · answered Jul 08 '13 at 17:16

2

$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];

answered Jul 08 '13 at 17:16

Greg

18,111
5
46
68

1

Interesting point here is that you are (correctly) using `$rose()` for the enabling condition. The reason you do that, and not just `req |-> ...` is so that you don't spawn a assertion thread every cycle that `req` is high, only the first. It's a big performance win. – Paul S Jul 11 '13 at 13:22

score 0 · Answer 2 · answered Jul 19 '13 at 00:01

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.

SVA for handshake

2 Answers2