第3章 SVA 仿真调度与采样机制
一句话导读：SVA 断言必须与 SystemVerilog 仿真调度表协同工作。采样时机若选择错误，属性将在旧值或新值之间“摇摆不定”，直接引发误报与漏报。
3.1 问题背景
一个断言包含两个关键时刻：采样时刻与求值时刻。在真实仿真器中，这两个时刻由“事件调度区域”管理。若把断言写进普通 always 块，并用阻塞赋值更新信号，SVA 可能在 Active 区读到尚未稳定的数据。
典型风险示例：
always @(posedge clk) begin
a_data = b_data; // 阻塞赋值，可能在采样前改变信号
if (a_data)
assert (c_data); // 采样时刻不可控
end因此，理解 Preponed、Active、Observed、Reactive 四个关键调度区域，是 SVA 工程实战的起点。
3.2 核心概念
SVA 在 Preponed 区采样，在 Observed 区求值。这个机制保证属性检查所用的信号值，都是时钟沿之前的稳定“旧值”。
要点：SVA 中的普通信号，如
sig_a，在 Preponed 区取当前快照；$past(sig_a) 也基于 Preponed 采样。这保证断言看到的是稳定值，而不是组合逻辑中间态。
3.3 原理机制
SystemVerilog 仿真标准将每个时间戳内的活动划分为多个区域。SVA 只依赖其中若干关键区域：
- Preponed：时钟沿之前瞬间，信号值不再变化，SVA 在此完成输入采样。
- Active / Inactive / NBA：RTL 进程执行，阻塞与非阻塞赋值更新，组合逻辑传播。
- Observed：SVA 属性被激活并进入求值阶段，与 RTL 更新隔离。
- Reactive：断言响应执行，包括报告打印、失败分支、外部调用。
3.4 流程步骤
- 仿真推进到时钟边沿。
- 在 Preponed 区对所有属性信号采样，形成“旧值快照”。
- 在 Active 区运行 RTL 逻辑，更新信号状态。
- 在 Observed 区执行属性检查，必要时调用
$past、$stable。 - 在 Reactive 区输出断言结果，更新覆盖率信息。
3.5 案例说明
示例：握手协议检查
property p_req_gnt;
@(posedge clk) disable iff (!rst_n)
req |=> gnt;
endproperty
assert property(p_req_gnt)
else $error("request without grant");req 在 Preponed 区被采样为高；在下一拍 Observed 区检查 gnt 是否也为高。即使 Active 区中 gnt 被同步更新，断言结果也不会被干扰。
3.6 调度区与 SVA 应用总结
| 调度区 | 仿真行为 | 对 SVA 的意义 |
|---|---|---|
| Preponed | 采样信号旧值 | a、$past(a) 的稳定读入口 |
| Active / Inactive / NBA | RTL 进程更新 | 与断言求值隔离，避免采样竞争 |
| Observed | 断言属性求值 | assert property 的唯一评估入口 |
| Reactive | 执行断言后动作 | else $error 等分支在此运行 |
3.7 误区提醒
请勿：
- 在
always_ff中直接使用if判断断言成功或失败，容易干扰 Preponed 采样。 - 让断言表达式引用阻塞赋值产生的中间信号，避免采样到未更新值。
- 忽略
disable iff，导致复位窗口期间误报失败。 - 将
$sampled与$past混用，二者帧对齐规则不同。
3.8 实战清单
- 所有断言都写成
property ... endproperty结构。 - 统一使用
@(posedge clk)作为采样时钟事件。 - 将
assert property放在 program 块中，与 RTL 逻辑隔离。 - 检查关键信号前使用
disable iff排除复位窗口。 - 如需手动采样，使用
$sampled(signal)并确认采样时刻与时钟沿对齐。 - 打开仿真器波形，观察 Preponed 采样点位置，确认断言时序符合预期。