SystemVerilog断言校验握手期间num变量值不变未触发问题求助

原有代码不触发的核心原因 #

• 仅定义了property结构，没有编写assert property实例化语句，仿真器不会自动执行未被实例化的断言逻辑
• 使用|=> 延迟一拍开始校验，会漏掉valid上升沿当前周期的num变化场景
• 部分场景下until_with语义匹配不符合预期，若valid在ready到来前拉低，会导致断言一直处于挂起状态，既不通过也不失败

正确实现代码 #

基础版（符合标准总线规则：valid拉高后保持至ready拉高） #

property check_num_stable_during_handshake;
  logic [15:0] local_num;
  @(posedge clk) 
    // 捕获valid上升沿时刻的num值
    ($rose(valid), local_num = num) 
    |-> 
    // 从当前周期开始，num保持不变直到ready上升沿出现，且ready上升沿当前周期num仍稳定
    num == local_num until_with $rose(ready);
endproperty

// 必须实例化断言才会在仿真中执行
ASSERT_NUM_STABLE: assert property(check_num_stable_during_handshake)
  else $error("num changed at time %0t, expected 0x%0h, got 0x%0h", $time, $past(local_num), num);

兼容版（覆盖valid提前拉低的异常场景） #

如果需要校验valid拉高后、无论是否等到ready，只要valid处于高电平阶段num就不能变化，可以使用如下写法：

property check_num_stable_while_valid_high;
  logic [15:0] local_num;
  @(posedge clk) 
    ($rose(valid), local_num = num) 
    |-> 
    num == local_num throughout (valid[*1:$] ##1 ($fell(valid) || $rose(ready)));
endproperty

额外排查点 #

如果修改后仍不触发，可按以下顺序排查：

• 确认clk、valid、ready信号的采样时钟域一致，不存在跨时钟域导致的边沿未被检测到的问题
• 若为连续传输场景（valid在ready拉高后保持高电平直接发起下一次传输），可将触发条件从$rose(valid)改为valid && !$past(ready)，适配连续传输的num捕获逻辑

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