时间戳

首页 > 解决方案 > SVA：验证不同时钟域中的稳定信号

system-verilog - SVA：验证不同时钟域中的稳定信号

问题描述

我的问题在以下论文“Asynchronous Behaviors Meet their Match with SystemVerilog Assertions”中得到了完美的描述：

考虑图 8 中的场景，其中选通信号在 src_clk 域中生成，并且必须在 dst_clk 域中稳定至少 3 个周期。断言必须检查选通信号是否保持稳定，而且它有足够的建立和保持时间在 dst_clk 域中进行采样。

图 8

然后作者提出以下断言来克服这个问题：

assert property (
    @(posedge src_clk) $rose(strobe) |-> (
        strobe[*1:$] ##1 1 )
    ) intersect (
        ##1 @(posedge dst_clk) strobe[*3]
        ##1 @(posedge src_clk) 1
    )
 );

我的问题是 Cadence incisive 15.20 和 Synopsys VCS 2014.10 都抱怨在相交中使用了多个时钟：

精辟 15.20：多时钟上下文中的无效运算符和/或操作数。

Synopsys VCS 2014.10：“相交”运算符的右操作数中预期的单时钟序列，找到了多时钟序列。

https://www.edaplayground.com/x/wGE

然而，当我使用 Aldec Riviera Pro 2017.02 编译时它确实有效，所以我猜这只是一个工具限制。

有没有其他替代方法可以实现这一目标？

标签： system-verilogsystem-verilog-assertions

解决方案

我发现使用胶合逻辑来避免复杂的属性很有帮助。

在这种情况下，我会计算 dst_clk 时钟并执行以下操作：

unsigned reg [7:0] dst_clk_conter_width;
parameter counter_width = 256;

always @(posedge dst_clk) 
  dst_clk_counter <= dst_clk_counter +1;

property prop;
  @(posedge src_clk or posedge dst_clk)
  $rose(strobe) |-> 
    (1,strobe_rise_dst_clk_num = dst_clk_counter) 
    ##[1:$] strobe
    ##1 strobe && (dst_clk_counter  = (strobe_rise_dst_clk_num + 3) % counter_width)
endproperty

解释：

第一行捕获当前计数器值，第二行确保频闪不会下降，最后一行检查我们是否已经通过了 3 个 dst 时钟

推荐阅读