以下协议的 SVA

【问题标题】：SVA for the following protocol以下协议的 SVA
【发布时间】：2021-01-28 13:46:39
【问题描述】：

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

我编写了以下 SVA，但它没有捕获即时确认。我该如何解决这个问题

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

【问题讨论】：

你是怎么测试的？你有可重现的例子吗？

标签： system-verilog system-verilog-assertions

【解决方案1】：

查看您的断言，它不会捕获立即 ACK，因为您期望的序列不包括带有 !ack 的立即 ACK。我会将您的断言重写为：

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

【讨论】：