SVA for a handshake

Question

I am trying to write an SVA statement for a handshake procedure.

In my searches, I 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 “ready” signal may occur many cycles after the actual cycle is high. How do you make this statement, make sure that the “done” statement is approved at any time after the valid statement, without a valid deletion?

Answer 1

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

$rose will launch the statement on the leading req . [*1:$] means that the left side must be true for a range of 1 to unlimited hours. You can use [+] , which is equivalent to [*1:$] .

Some other styles of writing validation:

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

Answer 2

You also do not need SVA to make sure that with valid $ rose's this is not yet confirmed? If you do, then PLS will consider this SVA- $ rose (valid) | → ~ done ## 1 $ stable (~ done) [* 949: 950] ## [1: $] done;

The foregoing requires that it is not approved for the period followed by future approval.