第2章 形式化验证与传统动态仿真验证：差异与互补

2.1 问题背景

在传统数字IC验证流程中，动态仿真（Dynamic Simulation）通过施加激励向量来观测设计行为。该方法直观、易调试，但始终存在一个核心局限：覆盖不完备。有限时间内只能模拟有限场景，未观测到的路径仍可能潜伏缺陷。

形式化验证（Formal Verification）从数学层面出发，将设计与性质转换为逻辑公式，通过求解器穷尽分析。它可以证明“该性质在所有可达状态下成立”，或给出精确反例。二者既存在显著差异，更应形成互补。

2.2 核心概念

2.2.1 覆盖率完备性

• 动态仿真：覆盖率依赖激励向量是否触达关键状态与分支。“仿真通过”只代表当前激励集下的行为正确，未激励路径仍是盲区。
• 形式化验证：验证工具自动遍历状态迁移关系，针对断言给出数学证明；若属性证明为真，则所有可达状态均满足该属性，即“100% 可达覆盖”。

2.2.2 反例描述

• 动态仿真：失败波形只能说明“当前激励下行为异常”，根因需要人工分析定位。
• 形式化验证：若属性不成立，工具自动给出反例轨迹（counterexample trace），从初始状态开始，精确展示导致性质破坏的输入序列。

2.2.3 适用场景

• 形式化验证：控制密集型逻辑、协议状态机、FIFO/存储一致性、跨时钟域握手、安全属性。
• 动态仿真：数据通路、复杂算法、视频/音频处理、大规模SoC集成、随机回归。

2.2.4 资源开销

• 动态仿真：大量CPU、存储和长回归周期；覆盖率增长后期收敛缓慢。
• 形式化验证：主要消耗内存与求解时间，可能遭遇状态爆炸；但证明完成后无需重复运行。

下图给出两种验证路径的对比框架：上方区分方法论，中部描述各自覆盖特性，底部体现互补融合方向。