system verilog - SVA for the following protocol

Question

I have to write a single SVA for the complete protocol shown in this image

I wrote the following SVA but it doesn't capture the immediate ack. How do I fix that

@(posedge clk) 
  $rose(val) |=> 
    ( $stable(data) && !ack && val ) ##[1:64] ( ack && val ) ##1 ( !ack && !val ) 

question from:https://stackoverflow.com/questions/65938352/sva-for-the-following-protocol

Answer 1

Looking at your assertion, it won't capture the immediate ACK because you are expecting a sequence excluding an immediate ACK with !ack. I would re-write your assertion as:

sequence seq;
  $stable({address, data}) ##[0:63] (val && ack && $stable({address, data})) ##1 !ack ##1 !val;
endsequence
 
property p;
  @(posedge clk) 
     $rose(val) |=> seq;
endproperty

as_protocol : assert property(p);