System Verilog Assertions, SVA

Question

Im writing assertions for a handshake protocol where there can be back to back requests and acks. Acks can come between 1 to 5 cycles after req. How can I use assertions to make sure there is 1 ack for every req while also taking glitching on req or ack into account ?

property p1: @(posedge clk) req ##[1:5] ack ; endproperty

property p2: @(posedge clk) $rose(ack) |-> $past(req,5);

Im not sure if this keeps 1-to-1 mapping of req vs ack.

Answer 1

Can there be two requests before an ack? If not I would write :

property p_test;
@(posedge clk)
$rose(req) |=> !req[*0:$] ##0 ack;
endproperty

It works if req is pulse only

Answer 2

Property2 below is not in sync with property 1.

property p2: @(posedge clk) $rose(ack) |-> $past(req,5);

You are saying that ack must have had a request 5 clocks earlier. But property 1 says that req followed by ack is valid.

I think you need a id with a request that you can match when the ack happens.

    sequence s_ack_check;
        byte id;
        (req && id == ack_id) ##[1:5](ack && ack_id == id);
    endsequence

Answer 3

I take it you meant that there could be multiple reqs before any acks? If so, the solution needs either property variables or helper logic. Formal properties don't have memory or counters (without using variables).

Here's some code if you want to use helper logic:

Assume you allow at most 15 outstanding and it takes at most 25 clocks to get all acks:

logic [3:0] req_cnt, ack_cnt;
always @ (posedge clk) if (rst) req_cnt <= 0; else req_cnt <= req_cnt + req;
always @ (posedge clk) if (rst) ack_cnt <= 0; else ack_cnt <= ack_cnt + ack;

assert property (@ (posedge clk) disable iff (rst) sync_accept_on(req) ##25 req_cnt == ack_cnt);

Count the requests and acks. Then assert that after 25 cycles of no req, the req_cnt == ack_cnt.

If there's never more than 1 req outstanding, the logic is much simpler. Please clarify if that is the case.