第2章 形式化验证与动态仿真对比：激励依赖、穷举能力、收敛速度
本章学习任务：掌握形式化验证与动态仿真在 激励依赖、穷举能力、收敛速度 三个核心维度上的差异，能够在 IP 模块验证中合理选择方法组合。
2.1 问题背景：为什么必须对比？
动态仿真统治验证环境多年，但覆盖率漏洞时有发生；形式化验证以数学证明弥补盲区，却在规模与收敛上受限。验证工程师常面临一个选择：哪些属性用仿真？哪些属性用形式化？ 对比这两种方法的本质差异，是选型的第一步。
2.2 核心概念
- 动态仿真（Dynamic Simulation）：通过 Testbench 向 DUT 注入激励向量，比较输出响应与预期值。
- 形式化验证（Formal Verification）：将设计与属性转化为数学问题，用求解器对全部状态空间进行证明或反例搜索。