第1章 形式化验证基础与收敛优化全景：核心概念、原理机制、实战要点

1.1 问题背景

形式化验证以数学推理代替动态仿真，能够在全输入空间内证明设计行为的正确性。然而，工程实践中验证完备性并非“一证就灵”。引入覆盖率分析后，我们需要回答三个关键问题：

• 被验证的属性是否覆盖了真正重要的设计行为？
• 验证环境需要多长时间才能达到覆盖率收敛？
• 当覆盖率未达 100% 时，如何判断下一步动作？

这三个问题构成了覆盖率驱动的验证收敛的出发点，也是本课程 30 章内容的主线。

1.2 核心概念

• 形式化验证（Formal Verification）：基于逻辑与模型论，对电路或协议模型进行穷尽性验证。
• 属性（Property）：描述设计规约的形式化断言，是验证任务的输入和判据。
• 覆盖率（Coverage）：验证空间被探索或证明的比例，衡量验证完备性。
• 收敛（Convergence）：覆盖率随迭代推进不断逼近目标的演化过程。
• 反例（Counterexample）：违反属性的具体输入序列，是缺陷定位的重要证据。

1.3 覆盖率收敛流程框架

下图给出形式化验证覆盖率收敛的完整闭环：从设计建模到策略优化迭代，共五个关键环节。