systemverilog assertion 中交叠蕴含的使用问题

Question

编写assertion如下：

    property  prop1(busy_out,aclk_cg);
        //@(posedge sys_clk) aclk_cg===0 within busy_out===0;
        //@(posedge sys_clk) busy_out===0 throughout aclk_cg===0;
        @(posedge sys_clk) disable iff (acg_en===0)  $fell(busy_out) |-> $stable(aclk_cg)[*1:$] ##1 busy_out;
    endproperty

波形如下：

在log中busy_out出现下降沿之后，aclk_cg有个高电平到低电平的过程，但是这里没有出现offending，这是为什么呢？ 交叠蕴含不是说是在同一个周期生效嘛？为什么在这里没有报错呢？

Answer 1

引自免费微信小程序：皆我百晓生

从您提供的信息来看，您在SystemVerilog中的assertion可能没有正确地捕捉到预期的行为。交叠蕴含（overlapped implication）用于检查两个事件在同一时钟周期内发生的情况。在这个例子中，您期望$fell(busy_out) 和 $stable(aclk_cg)[*1:$] 在一个时钟周期内同时发生。

然而，在您的assertion中，您似乎将这两个条件分开了，分别使用了不同的语句。为了更好地理解问题，让我们先澄清几个点：

1. @(posedge sys_clk) aclk_cg===0 within busy_out===0; 这个断言检查的是aclk_cg在busy_out为0的同一时钟周期内变为0。
2. @(posedge sys_clk) busy_out===0 throughout aclk_cg===0; 这个断言检查的是在aclk_cg为0的整个持续期内，busy_out都保持为0。
3. @(posedge sys_clk) disable iff (acg_en===0) $fell(busy_out) |-> $stable(aclk_cg)[*1:$] ##1 busy_out; 这个断言在acg_en为0的情况下，当busy_out下降沿发生后，它期望aclk_cg在接下来的一个时钟周期内稳定不变，并且与busy_out的下一个状态相关联。

根据您的描述，当busy_out下降沿发生后，aclk_cg有一个高电平到低电平的过程，但没有触发断言错误。这可能是因为上述断言并没有正确地捕获这个特定情况。要解决这个问题，您可以尝试合并这些断言以确保在同一时钟周期内检查这两个条件。一种可能的改进方法是使用并行断言（|）：

property prop1(busy_out, aclk_cg, sys_clk);
    @(posedge sys_clk)
        disable iff (acg_en === 0) (
            ($fell(busy_out) && $stable(aclk_cg)[*1:$]) |
            ((busy_out === 0) && (aclk_cg === 0))
        );
endproperty

这个新的断言首先检查$fell(busy_out)并且$stable(aclk_cg)[*1:$]是否在同一个时钟周期内发生，如果acg_en不为0，则跳过此检查。此外，它还检查busy_out和aclk_cg在同一时钟周期内都为0的情况。这样应该能更准确地捕捉到您期望的行为。

请注意，如果您的目标是检查busy_out下降沿之后紧接着的时钟周期内aclk_cg是否稳定为0，那么原始断言中的第三个部分已经足够了。问题可能是出在其他地方，比如测试平台配置、信号同步等问题。

如果您仍然遇到问题，建议您检查以下几点：

• 确保所有信号都在正确的时钟域中，并且它们之间的关系被正确处理（例如，使用同步器、异步FIFO等）。
• 检查acg_en信号的状态，确保其在预期的时间内为0。
• 如果有多个时钟域，确保跨域的信号转换正确无误。
• 检查仿真设置，特别是时钟偏移和采样时间，确保它们不会影响断言的结果。

如果以上步骤都无法解决问题，您可能需要提供更多的上下文信息，如测试平台配置文件和详细的波形数据，以便进行更深入的分析。