以下协议的 SVA

问题描述

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 ) 

解决方法

查看您的断言，它不会捕获即时 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);