形式化验证中的常见错误类型与故障模型

形式化验证和仿真调试的最大区别，在于你碰到 FAIL 时不能直接打开波形做“长时间探索式排查”。证明引擎给出的是一个反例轨迹和一组已验证的约束集合，你必须快速判断：这个失败到底来自属性写错、约束失真、实现缺陷、环境建模问题，还是单纯因为资源不足？

核心概念：验证失败的五层归因

在形式化验证过程中，FAIL 不等于“设计错了”。一个反例可能来自以下任意一层：

• 属性层：property 未准确表达设计规格，导致断言语义错误。
• 约束层：assume/constraint 过强或过弱，导致环境模型与真实场景不符。
• 实现层：RTL 或门级网表存在真实逻辑缺陷、边界遗漏或状态机死锁。
• 建模层：验证平台的抽象粒度、时钟/复位建模、DUT wrapper 有问题。
• 资源层：状态空间爆炸或引擎超时，尚未形成完备结论。

原理机制：反例到底在告诉引擎什么？

从底层视角看，验证引擎返回的 FAIL / PASS / UNKNOWN 分别对应不同的数学事实：

反例轨迹是“结果”，故障模型是“解释”。一个反例在定位过程中通常经历四个推演阶段：

1. 触发：某个输入序列激活使能条件。
2. 传播：内部状态变化导致关键信号翻转。
3. 违例：property 前提满足但后果不成立。
4. 归因：判断违例根源在属性、约束、实现还是建模。

流程步骤：五步定位法

1. 保存证据：导出反例波形、运行日志和当前 property/constraint 集合。
2. 属性校验：把 property 还原成“可观察行为描述”，排除属性自身语义错误。
3. 约束盘点：检查 assume 在反例中的激活情况，判断约束是否过强/过弱。
4. 信号追踪：从反例末端向前回溯 2~5 个周期，找到第一个异常翻转点。
5. 最小复现：简化输入序列或复位过程，获取最短反例轨迹。

案例说明：同一类失败，两种不同根因

案例 A：FIFO 下溢——设计实现错误，真缺陷

property p_fifo_no_underflow;
  @(posedge clk) rd_en |-> (rd_ptr != wr_ptr);
endproperty

验证结果 FAIL。反例中 rd_en=1、rd_ptr=0、wr_ptr=0，即 FIFO 为空时读端口仍发出读请求。进一步检查发现 RTL 中的读信号只受后级 handshake 控制，未与 empty 标志做 gating。判定为实现层故障。

案例 B：总线响应周期约束缺失——属性建模错误，误报

property p_bus_idle;
  @(posedge clk) bus_req |-> event_ready;
endproperty

验证结果 FAIL。反例中 bus_req 拉高后，event_ready 在第 3 拍才拉高。设计规格允许 1~5 拍响应，但 property 写成了“下一拍必须响应”。修正为带窗口的属性：

property p_bus_idle_fixed;
  @(posedge clk) bus_req |-> ##[1:5] event_ready;
endproperty

验证通过。这是属性层故障，不能直接修改设计。

表格总结：错误类型 × 故障模型对照

误区提醒

• 误把 UNKNOWN 当 PASS：引擎超时只代表“没找到问题”，不代表“没有问题”。
• 看到 FAIL 就改 RTL：案例 B 中改设计会让正确功能迁就错误断言，造成功能退化。
• 忽略约束覆盖率：约束过强会让反例和通过结果都失去工程意义。
• 只看反例尾部：根因通常发生在反例起点附近，而不是违规点附近。
• 不区分安全/活性失败：safety 失败有有限反例，liveness 失败往往与环、等待状态有关，定位方法不同。

实践清单

• 每次 FAIL 保存 3 类现场：反例波形、运行日志、证明引擎版本信息。
• 先做“属性自检”：将 property 与规格文档逐条映射。
• 为每个 assume 生成覆盖率报告，剔除无效或冗余约束。
• 记录反例长度（trace length），越短越适合人工分析。
• 修复后重跑完整 proof，避免用 shortcut bound 代替全证明。