SystemVerilog断言未按预期触发失败的原因排查

你的断言代码：

$rose(req) |=> !req[*1:10] until ack ##1 !ack;

没按你预期报错，核心是你对SVA运算符的语义、写法逻辑存在几个认知偏差，具体如下：

• 弱until天生不要求右操作数必须发生
  SVA里默认的until是弱直到属性，规则很明确：只要左操作数一直保持成立，哪怕右操作数永远不匹配，仿真结束也不会判失败。
  你的测试里ack拉高之后一直没拉低，ack ##1 !ack这个两周期事件从来没成功匹配过，弱until就会一直等，不会主动报错。真要强制右操作数必须出现，得用强直到s_until，但就算换了，你现在的写法也实现不了想要的效果。
• 左操作数写法完全不对，根本做不到持续检查
  你本来想让!req[*1:10]实现「ack来之前每个周期req都为低，最多撑10个周期」，但实际上!req[*1:10]是个有界的单次匹配序列：只要$rose(req)之后第一个周期采到!req，就满足了最小1次重复的要求，这个子部分直接就匹配过了，根本不会盯着后面的周期查req是不是低，也卡不住10个周期的上限。
• 对until的触发时机理解错了
  P until Q是要等Q整个序列完全匹配上，才会结束左操作数的检查，不是Q的起始条件满足就停。你写的Q是ack ##1 !ack，必须凑齐「某周期ack=1、下一周期ack=0」两个条件才算匹配完成。你测试里ack一直是高，Q永远匹配不完，until的线程当然会一直跑，也不会触发你以为的「ack来了就查下周期拉低」的逻辑。

可实现预期逻辑的写法 #

如果要落地你说的校验规则：检测到$rose(req)后，下一个周期开始最多10个周期req必须为低；这期间只要ack拉高，下一个周期ack必须拉低，可以直接这么写：

$rose(req) |=> (!req throughout ##[1:10] ack) ##1 !ack;

这里用throughout保证ack到来前所有周期req都为低，##[1:10] ack约束ack必须在1到10个周期内出现，最后##1 !ack卡ack拉高后下一周期必须拉低，你那个ack持续拉高4个周期的场景会直接报失败。

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