3. 时钟与复位建模

在形式属性验证中，时钟与复位不是“背景条件”，而是决定属性是否成立、何时成立、在哪个采样点成立的核心建模对象。很多看似失败的属性，根源并不在RTL功能错误，而在于时钟域划分不清、复位释放时刻未对齐、或复位序列与属性采样窗口错位。本节围绕三个关键问题展开：多时钟域如何建模、异步复位同步释放如何表达、复位序列如何影响属性验证结果。

一、多时钟域建模：先明确“谁在哪个时钟下采样”

形式验证工具通常要求为每个时钟定义独立的时钟周期或时钟约束。当设计包含多个时钟域时，属性必须明确指定其采样时钟。例如，一个跨时钟域握手设计包含 clk_a（100MHz，周期10ns）和 clk_b（50MHz，周期20ns），若属性写成 @(posedge clk_a) req_a |-> ##[1:3] ack_b，则断言在 clk_a 域采样，但 ack_b 是 clk_b 域信号，其变化相对于 clk_a 是异步的。此时 ##[1:3] 的延迟窗口在 clk_a 周期下计算，可能永远无法覆盖 ack_b 的真实响应时间。

正确的做法是：跨时钟域属性应使用“同步器输出侧”的时钟采样，或显式使用 $rose/$fell 配合 @(posedge clk_b) 单独描述接收侧行为。若工具支持多时钟属性，可写成两个独立属性：发送侧属性在 clk_a 下检查请求保持，接收侧属性在 clk_b 下检查应答生成。这样每个属性只在其所属时钟域内采样，避免异步采样导致的假失败。

二、异步复位同步释放：从电路到属性的完整表达

异步复位同步释放（Asynchronous Reset Synchronous Release）是工程中最常见的复位策略。其典型电路由两级触发器串联构成：第一级触发器的异步复位端接 rst_n，第二级触发器同样接 rst_n，但两级触发器的数据端都接高电平，输出 rst_sync_n 作为系统同步复位。当 rst_n 拉低时，两级触发器立即异步清零，rst_sync_n 立刻为低；当 rst_n 拉高时，第一级在 clk 上升沿采样到高电平，第二级再延迟一个周期采样到高电平，因此 rst_sync_n 在 rst_n 释放后经过两个时钟周期才变为高电平。

在SVA中，这一行为需要分两段描述。异步断言部分：@(posedge clk or negedge rst_n) !rst_n |-> !rst_sync_n，表示只要 rst_n 为低，rst_sync_n 必须为低，且该属性在 rst_n 下降沿立即触发，不等待时钟。同步释放部分：@(posedge clk) $rose(rst_n) |-> ##[1:2] $rose(rst_sync_n)，表示 rst_n 上升沿后，rst_sync_n 应在1到2个时钟周期内上升。注意这里使用 ##[1:2] 而非固定 ##2，因为实际电路中第一级和第二级触发器的采样时刻可能因时钟偏斜或工具建模差异而略有浮动，窗口化断言更稳健。

三、复位序列对属性验证的影响

复位序列不仅影响电路初始状态，还直接影响属性的“起始采样点”。形式验证工具在证明属性时，会从复位状态开始搜索反例。如果复位序列建模不完整，工具可能从一个未定义的中间状态开始验证，导致属性被错误地“证明通过”或“证明失败”。

常见问题有三类。第一，复位释放时刻未约束。若 rst_n 在仿真或形式验证中可以在任意时刻释放，工具会尝试所有可能的释放时刻，其中一些时刻可能对应真实硬件中不会出现的亚稳态窗口，从而产生假反例。解决方法是在验证环境中添加复位释放约束，例如 assume property (@(posedge clk) $rose(rst_n) |-> rst_n_stable_for >= 2)，限制释放后至少保持两个周期稳定。

第二，多时钟域复位释放顺序未建模。若 clk_a 域和 clk_b 域共享同一个 rst_n，但各自有独立的同步释放电路，则两个域的 rst_sync_n 可能在不同时刻释放。若属性假设两个域同时退出复位，就会产生假失败。正确做法是为每个域分别建模同步释放，并在跨域属性中显式引用各自的 rst_sync_n 作为前提条件。

第三，复位期间属性被意外激活。SVA默认在复位期间不检查属性，但若使用了 disable iff 却写错了条件，例如 disable iff (!rst_n) 写成 disable iff (rst_n)，则属性会在复位期间被激活，而在正常工作时被禁用，完全颠倒。建议统一使用 disable iff (!rst_n) 或 disable iff (rst_sync_n === 1'b0)，并确保复位信号在属性中作为“禁用条件”而非“触发条件”。

四、复位序列建模的实操建议

在形式验证环境中，复位序列通常通过 initial 块或约束文件定义。以下是一个可参考的复位序列建模片段，用于约束 rst_n 的释放行为：

// 复位序列约束示例（形式验证环境）
// 假设 clk 周期 10ns，rst_n 低有效
initial begin
  rst_n = 1'b0;          // 上电复位
  #25;                   // 保持低至少 2.5 个周期
  rst_n = 1'b1;          // 释放复位
end

// 属性中的复位禁用条件
property p_handshake;
  @(posedge clk) disable iff (!rst_sync_n)
  req |-> ##[1:3] ack;
endproperty

// 复位释放稳定性假设
assume property (@(posedge clk) $rose(rst_n) |-> ##[1:2] rst_n);

注意 disable iff (!rst_sync_n) 与 disable iff (!rst_n) 的区别：前者在同步复位释放后才开始检查属性，后者在异步复位释放后立即开始检查，可能覆盖同步器尚未稳定的窗口。对于跨时钟域设计，建议统一使用同步释放后的复位信号作为禁用条件，确保属性只在所有相关时钟域都退出复位后才生效。

五、复位序列与属性收敛的关系

复位序列建模的完整性直接影响属性证明的收敛速度。若复位释放时刻未约束，工具需要搜索所有可能的释放时刻，状态空间会显著增大。通过添加 assume 约束限制复位释放后的稳定窗口，可以缩小搜索空间，加速收敛。例如，约束 rst_n 释放后至少保持10个周期为高，工具就不需要探索释放后立即再次拉低的场景，从而减少无效反例。

此外，对于多时钟域设计，若两个时钟域的复位释放顺序未约束，工具会尝试所有可能的交错顺序。若实际硬件中两个域共享同一个 rst_n 且同步释放电路结构相同，则释放顺序由各自时钟沿决定，工具需要覆盖两种顺序。若在验证环境中添加 assume 约束指定释放顺序，可以进一步缩小搜索空间。但需注意，约束必须是真实硬件中成立的，否则会掩盖真实缺陷。

总结来说，时钟与复位建模的核心是：每个属性明确采样时钟，跨域行为拆分为单域属性；异步复位同步释放分两段描述，异步段用 negedge rst_n 触发，同步段用 ##[1:2] 窗口；复位序列通过 initial 块和 assume 约束建模，确保工具从正确的初始状态开始验证。这三者共同决定了属性验证的准确性和收敛效率。