如何用SVA编写属性：sig_1有效期间sig_2需完成完整跳变

问题背景 #

当sig_1断言（高电平）至少X个周期时，sig_2必须完成至少一次完整的断言（即出现一次上升沿+下降沿）。原编写的SVA属性未达到预期效果：

property prop_sig_2_while_sig_1;
    @(posedge clk)
        $rose(sig_1) ##[0:$] $rose(sig_2) ##[0:$] $fell(sig_2) ##[0:$] $fell(sig_1);
endproperty : prop_sig_2_while_sig_1

问题分析 #

原属性的核心缺陷：

• 未约束sig_1在$rose到$fell期间保持高电平，可能出现sig_1中途降为低电平再拉高的误判
• 未区分sig_1持续时间不足X个周期的豁免场景（这种情况不需要检查sig_2）
• 序列逻辑无法保证sig_2的完整触发完全落在sig_1的断言窗口内

可行实现方案 #

方案1：用throughout+intersect精准约束 #

property prop_sig2_valid_during_sig1;
    @(posedge clk)
    // 触发条件：sig_1上升沿，且后续至少持续X个周期才下降
    $rose(sig_1) |=> (sig_1 throughout (##[X-1:$] $fell(sig_1)))
    // 要求sig_2的完整触发（上升后至少1个周期再下降）与sig_1的高电平窗口完全重叠
    intersect ($rose(sig_2) ##[1:$] $fell(sig_2));
endproperty

assert property (prop_sig2_valid_during_sig1) 
else $error("Error: sig_2未在sig_1断言周期内完成完整触发");

方案2：用within简化逻辑表达 #

property prop_sig2_valid_during_sig1;
    @(posedge clk)
    // 当sig_1的断言持续至少X个周期时
    ($rose(sig_1) ##[X-1:$] $fell(sig_1))
    // 要求sig_2的完整触发发生在sig_1的断言窗口内
    implies ($rose(sig_2) ##[1:$] $fell(sig_2) within ($rose(sig_1) ##[0:$] $fell(sig_1)));
endproperty

assert property (prop_sig2_valid_during_sig1) 
else $error("Error: sig_2未在sig_1断言周期内完成完整触发");

关键细节说明 #

• 周期数X的计算：##[X-1:$]是因为$rose(sig_1)发生在当前周期，之后经过X-1个周期，sig_1的高电平就至少持续了X个周期（比如X=3时，上升沿后至少2个周期再下降，总持续3个周期）
• throughout：强制sig_1在整个序列期间保持高电平，避免中途跳变导致的误判
• intersect/within：确保sig_2的上升和下降完全包含在sig_1的高电平窗口内，满足“sig_1断言期间sig_2至少断言一个周期”的要求
• 豁免场景：如果sig_1的持续时间不足X个周期，上述属性不会触发检查，符合需求

内容的提问来源于stack exchange，提问作者erng