📚 课程目录第3章形式验证基础概念

3. 形式验证基础概念

形式验证的核心不是“跑激励看波形”，而是把设计意图写成可被数学工具推理的属性，再让求解器在状态空间中穷尽搜索，给出“所有可能输入下都成立”的证明，或给出“存在一条路径使其失败”的反例。理解这一组概念之间的分工，是使用 VC Formal 的前提。

断言与属性：意图的两种表达粒度

断言（assertion）是写在 RTL 或绑定文件中的一条检查语句，它声明“在某个时刻，某个条件必须为真”。属性（property）是断言所描述的时间行为本身，可以跨越多个时钟周期，例如“请求发出后，最多 3 个周期内必须收到应答”。断言是属性的载体，属性是断言的语义内容。

在 SystemVerilog 中，立即断言在过程块中按当前时刻求值，适合组合条件检查；并发断言基于时钟采样，适合描述时序关系。VC Formal 主要处理并发断言，因为形式引擎需要把时间展开成状态转移序列。一个典型的属性写法如下：

property p_req_ack;
  @(posedge clk) disable iff (!rst_n)
  req |-> ##[1:3] ack;
endproperty

a_req_ack: assert property (p_req_ack);

这里 |-> 是重叠蕴含，##[1:3] 表示 1 到 3 个周期内。VC Formal 会把它翻译成自动机，并在所有可达状态上检查是否存在违反路径。

约束：把环境“关进笼子”

形式验证默认输入可以取任意值。如果不加限制，工具会探索大量现实中不可能出现的输入组合，导致证明失败或资源爆炸。约束（constraint）用于描述环境合法行为，例如“读和写不会同时有效”“地址必须落在有效区间”。约束不是检查目标，而是对输入空间的裁剪。

在 VC Formal 中，约束通常通过 assume property 或 assume 语句表达。需要特别注意：约束过强会把真实缺陷一起排除，约束过弱则证明无法收敛。工程上常把约束分为协议约束、配置约束和复位约束三类，并逐条评审其合理性。

覆盖：证明“检查到了该检查的地方”

覆盖（cover）回答的是“这条场景是否可达”。在形式验证中，覆盖属性用于确认某个状态、某条分支或某个时序组合确实存在可达路径。如果一条覆盖属性被证明不可达，说明约束可能过强，或者设计存在死代码。

VC Formal 支持 cover property 和 cover 语句。与仿真覆盖率不同，形式覆盖是“存在性证明”：工具要么给出一条到达该场景的路径，要么证明它永远不可达。后者往往比前者更有价值，因为它直接暴露了约束与设计之间的不一致。

证明与反例：两种确定性的结果

当 VC Formal 对一条断言返回 proven，意味着在所有满足约束的输入序列和所有可达状态下，该属性都成立。这是形式验证最强的结论，不依赖激励质量。

当返回 falsified，工具会给出反例（counterexample）：一条从初始状态出发、满足所有约束、最终使断言失败的波形。反例通常包含若干周期的信号取值，工程师需要沿着这条路径判断：是设计缺陷、约束缺失，还是断言写错。反例的长度和内容直接决定调试效率，因此 VC Formal 提供反例波形查看和信号追踪能力。

还有第三类结果 inconclusive，表示在给定资源或时间限制内无法得出结论。这通常由状态空间过大、约束不足或属性过于复杂引起，需要拆分属性、加强约束或调整证明策略。

有界证明与无界证明

有界证明（bounded proof）只检查从初始状态出发、在有限个周期内（例如 20 个周期）是否违反属性。它速度快，适合早期快速筛查，但结论是“在 20 个周期内未发现反例”，不能说明 21 个周期后是否安全。

无界证明（unbounded proof）则要证明属性在所有时间上都成立。VC Formal 通常通过 k-归纳、插值或抽象精化等引擎完成。无界证明的结论才是真正的“全证明”，但代价更高，可能需要更多计算资源和更精细的约束。

工程实践中常见的策略是：先用有界证明快速找到浅层反例，再逐步增加深度；当有界证明长时间无结果时，切换到无界证明引擎，并配合覆盖属性确认关键场景可达。

在 VC Formal 中的对应表达

把上述概念落到 VC Formal 工程中，通常形成如下对应关系：设计意图写成 SVA 属性；检查目标用 assert property；环境假设用 assume property；场景可达性用 cover property。VC Formal 的 vcFormal 命令或 GUI 流程会读取这些语句，并选择证明引擎。

一个可执行的检查清单如下，用于评审一组形式属性是否完整：

每条断言是否对应一条明确的设计需求，而不是重复 RTL 实现？
每条约束是否有书面依据，是否可能排除真实缺陷？
关键场景是否都有对应的覆盖属性，且覆盖属性已被证明可达？
有界证明深度是否足够覆盖协议最长延迟？
无界证明是否在合理资源内完成，未决项是否有拆分计划？
反例是否已定位到具体信号和周期，并区分设计问题与约束问题？

建议在项目初期先建立“断言—约束—覆盖”三张清单，再运行证明。这样即使工具返回 inconclusive，也能快速判断是约束不足还是属性过于复杂。

最后需要强调：证明与反例不是对立的，而是同一搜索过程的两种输出。有界证明适合快速迭代，无界证明适合签核；覆盖则保证你没有在“空集”上做证明。三者配合，才能让形式验证结论真正可信。