SystemVerilog断言：如何限制A&&!B连续32周期为真（FPV场景）

针对你提出的需求——禁止A && !B连续32个时钟周期为真（等价于A连续32个周期为真时B必须在该窗口内变为真），以下是几种适合形式化验证（FPV）场景的断言写法，均避免了xyz |-> 0这类否定蕴含写法：

写法1：正向约束连续序列的终止 #

assert property (@(posedge clk) 
    (A && !B)[*31] |-> !(A && !B));

这个断言的逻辑很直接：如果已经连续31个周期满足A && !B，那么第32个周期必须打破这个序列（即要么A为假，要么B为真）。它通过正向约束的方式，从根源上避免了连续32个A && !B的情况出现，完全符合你避免否定写法的要求，FPV工具能很好地分析这类断言，不会产生覆盖漏洞。

写法2：直接禁止目标序列（序列否定） #

assert property (@(posedge clk) 
    not ((A && !B)[*32]));

这种写法直观对应“不允许A && !B连续32个周期”的需求，虽然用了not操作符，但这是对序列的直接否定，不属于你要避免的xyz |-> 0这类否定蕴含形式，FPV工具对这类断言的支持也很成熟，不会出现覆盖问题。

写法3：明确约束B的出现窗口 #

如果你更想直接表达“A连续32个周期为真时，B必须在该窗口内出现”的原始逻辑，可以用within操作符：

assert property (@(posedge clk) 
    A[*32] |-> strong(B[->1] within A[*32]));

• A[*32]定义了连续32个周期A为真的序列；
• B[->1]表示B至少出现一次；
• within A[*32]限定B的出现必须在这32个A的周期范围内；
• strong用来确保B必须在该窗口内出现（而非等待窗口结束后），符合形式化验证的严谨性要求。

以上三种写法逻辑等价，你可以根据自己的阅读习惯和工具偏好选择。

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