SVA for the following protocol

0
votes

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 )
1
system-verilogsystem-verilog-assertions
how did you test? do you have a reproducible example? – Serge

1 Answers

1
votes

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);