无时钟使能场景下双异步复位的关联断言编写求助

嘿，我来帮你搞定这个异步复位的断言问题～首先得先拆解你的核心需求：只要Reset_a处于有效状态，Reset_b就必须也处于有效状态——不管Reset_a是刚触发还是已经持续有效，Reset_b要么已经处于有效状态，要么得立刻进入有效状态并保持。咱们先看看你写的断言存在的问题，再给出更精准的写法。

你的原断言的问题 #

你写的这段代码：

reset_assertion_check: assert property (@(posedge reset_a) $rose(reset_b) ##[*0:$] reset_b) else $error("reset error");

有两个关键缺陷：

1. 触发时机太局限：它只在reset_a的上升沿触发检查，没法覆盖reset_a持续有效期间的异常情况——比如reset_a一直保持有效，但reset_b中途意外失效了，这个断言根本不会触发检查。
2. 错误的跳变要求：$rose(reset_b)强制要求reset_b必须在reset_a上升沿时刻或之后产生一个上升沿，但如果reset_b在reset_a触发之前就已经处于有效状态（这完全符合你的需求），$rose(reset_b)会返回假，导致断言误报错。

推荐的断言写法 #

根据你的需求，我们需要只要Reset_a有效，Reset_b就必须有效，这里分两种常见的复位有效电平场景：

场景1：复位为高有效（reset_a/reset_b为1时有效）

// 核心断言：只要reset_a有效，reset_b必须同时有效
reset_a_implies_reset_b: assert property (
  @(*)  // 电平敏感触发，任何信号变化时都会检查
  reset_a |-> reset_b  // 蕴含关系：reset_a有效时，reset_b必须有效
) else $error("Reset_a is asserted but Reset_b is NOT valid!");

• @(*)：电平敏感触发，确保任何时刻只要reset_a的状态变为有效，或者reset_b状态发生变化时，都会立刻检查两者的对应关系。
• reset_a |-> reset_b：直接表达你的核心需求——当reset_a有效（为1）时，reset_b必须也有效（为1），不管reset_b是早就有效还是和reset_a同时触发。

场景2：复位为低有效（reset_a/reset_b为0时有效）

如果你的复位是低有效，只需要把电平判断反过来：

reset_a_implies_reset_b: assert property (
  @(*)
  !reset_a |-> !reset_b
) else $error("Reset_a is asserted but Reset_b is NOT valid!");

进阶：允许Reset_b在Reset_a触发后短暂延迟生效 #

如果你的需求可以放宽一点：允许reset_b在reset_a触发后有短暂延迟，但最终必须进入有效状态并保持（直到reset_a释放），可以用这个版本：

reset_a_implies_reset_b_eventually: assert property (
  @(posedge reset_a)
  strong( reset_b throughout (reset_a)[*1:$] )
) else $error("Reset_a is asserted but Reset_b never stays valid!");

• strong(...)：确保在reset_a持续有效的整个时间段内，reset_b最终会稳定保持有效状态（不会中途失效）。
• reset_b throughout (reset_a)[*1:$]：明确要求reset_b在reset_a的整个有效周期内都保持有效。

最后提醒 #

异步断言不需要依赖时钟，所以别用时钟沿触发（比如@(posedge clk)），用电平敏感触发（@(*)或@(reset_a)）才能准确覆盖异步复位的所有场景。

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