一、课程导论：形式化验证与动态仿真的定义、各自的优缺点、为什么需要结合、课程目标与学习路径

动态仿真，说白了就是给设计喂激励，然后看它怎么动。

你写一段 Verilog 或 SystemVerilog，搭一个 testbench，给时钟、给复位、给数据，然后跑仿真器。仿真器会模拟电路的行为，输出波形。你盯着波形看，或者用断言检查，确认设计对不对。

嗯，这就是我们每天都在做的事。我个人习惯用 UVM 搭验证环境，跑 regression，收集覆盖率。这套流程在业界已经非常成熟了。

动态仿真的优点：

动态仿真的缺点：

我的经验： 我曾经在一个 PCIe 控制器项目里，regression 跑了三个月，覆盖率 98%，结果流片回来发现一个 corner case——某个特定长度的包在特定链路状态下会丢数据。这个场景，仿真里从来没触发过。嗯，这就是动态仿真的天花板。

形式化验证，说白了就是不用跑仿真，直接用数学方法证明设计是对的。

你把设计描述成一个数学模型，把你要验证的属性（比如“总线仲裁器永远不会同时 grant 两个 master”）写成形式化断言。然后工具会用 SAT solver、BDD 或者模型检验算法，去穷尽地检查所有可能的状态空间。

如果工具说“通过”，那就是真的通过了——所有输入组合、所有状态、所有时序路径，一个不漏。

形式化验证的优点：

形式化验证的缺点：

注意： 形式化验证不是万能的。我曾经见过一个团队，花了两周时间试图用形式化验证一个 64 位浮点乘法器，结果工具直接爆内存。最后他们还是老老实实回去跑仿真。形式化验证要选对场景。

你想想看，动态仿真和形式化验证，其实是一对互补的兄弟。

动态仿真擅长验证复杂的大模块，但永远有遗漏的风险。形式化验证能保证完备性，但只能处理小模块或特定属性。

那为什么不把它们结合起来呢？

结合的核心思路：

我在一个 AI 芯片项目里用过这个思路。芯片有一个复杂的调度器，控制着 16 个计算核的任务分配。我们用形式化验证证明了调度器永远不会死锁、永远不会漏掉任务。而数据通路和计算核的交互，则用 UVM 仿真来覆盖。结果呢？流片一次成功，调度器零 bug。

  核心观点： 形式化验证 + 动态仿真，不是二选一，而是 1+1 > 2。形式化验证负责“证明正确”，动态仿真负责“验证功能”。两者结合，才能做到既快又稳。

这门课的目标很明确：让你学会在实际项目中，把形式化验证和动态仿真结合起来用。

具体来说，学完这门课，你应该能：

学习路径建议：

我的建议： 别急着上手工具。先花时间理解“为什么需要结合”这个核心问题。想清楚了，后面的学习会事半功倍。我见过太多人，工具用得溜，但遇到实际问题就不知道怎么选方案——就是因为没想清楚原理。

下面这张图，帮你理清本章的核心逻辑：

这张图展示了本章的核心逻辑：动态仿真和形式化验证各有优缺点，它们不是竞争关系，而是互补关系。结合的关键在于“取长补短”——用形式化验证的完备性弥补仿真的遗漏风险，用仿真的灵活性弥补形式化的状态爆炸问题。

嗯，这就是我们这门课要讲的核心思想。后面的章节，我们会一步步深入，从断言语法到工具使用，从单一方法到混合流程，最终让你能独立完成一个项目的混合验证方案设计。

可可精品资料库