陷阱四：形式验证（Formal）环境搭建错误

形式验证，圈里人常叫它 Formal。听起来挺高大上，说白了就是用数学方法证明你的设计和参考模型在功能上完全等价。不用跑仿真，不用等波形，理论上能覆盖所有输入组合。

但理想很丰满，现实很骨感。我见过太多团队，Formal 环境搭得轰轰烈烈，跑了一周说「验证通过」，结果流片回来发现功能不对。查到最后，问题出在环境搭建上——比对点设错了。

嗯，今天我们就聊聊这个坑。

Formal 验证的核心逻辑很简单：

这个「比对点」，就是工具具体去比哪些信号、在什么时机去比。比对点设错了，工具比对的就是两堆不相干的数据，结果自然毫无意义。

⚠️ 常见误区： 很多人以为 Formal 工具会自动识别所有输出端口作为比对点。其实不是。工具默认只比对顶层输出，内部状态、中间变量、甚至某些使能信号都需要手动指定。

有一次，我验证一个 FIFO 控制器。顶层输出只有两个信号：full 和 empty。Formal 跑完，报告说完全等价。我总觉得不放心，手动翻了翻波形——发现内部有一个 wr_ptr 指针，参考模型和 RTL 在某个边界条件下差了 1。

为什么会这样？因为 wr_ptr 不是顶层输出，工具根本没比它。而 full 和 empty 恰好在这个边界条件下仍然一致——纯属巧合。

  教训： 内部状态寄存器、状态机编码、计数器，这些都要加入比对点。不要只看顶层输出。

另一个项目，验证一个流水线乘法器。参考模型是组合逻辑，RTL 是三级流水。我把所有输出信号都设成了比对点，结果 Formal 报了几百个 mismatch。

我一开始以为是 RTL 写错了，查了三天。后来才发现——参考模型是 零延迟 输出，RTL 要等三个时钟周期才出结果。工具在每个时钟周期都去比，当然全错。

解决方案： 对于流水线设计，比对点要设置延迟匹配。比如用 assume 或 cutpoint 告诉工具：「请在第 3 个时钟周期之后才开始比对这组信号」。

这个坑特别隐蔽。参考模型通常用软件实现，复位后所有寄存器清零。但 RTL 里有些寄存器是 异步复位，有些是 同步复位，还有些复位值不是 0 而是 0x5A。

Formal 工具在复位期间就开始比对，结果自然 mismatch。很多人第一反应是「RTL 有 bug」，其实只是复位行为没对齐。

  建议： 在 Formal 环境中，明确告诉工具复位阶段持续多少个周期，复位期间不要比对。或者统一将参考模型的复位行为改成与 RTL 完全一致。

我个人习惯按以下步骤来，基本能避开 90% 的坑：

一个小技巧： 我曾经在环境里加了一个「哨兵信号」——一个永远不会被用到的 dummy 输出。如果 Formal 报告这个哨兵信号也通过了，说明工具可能根本没认真比对。听起来有点土，但确实帮我抓出过两次工具配置错误。

下面这张图总结了 Formal 环境搭建中，比对点相关的关键环节和常见陷阱：

最后，分享几条我这些年总结出来的经验：

不要迷信工具的默认设置。 工具默认只比顶层输出，但很多 bug 藏在内部状态里。手动把关键内部信号加进去。
比对点数量要心中有数。 如果你设了 50 个比对点，工具报告说「全部通过」，但你预期应该有 80 个——那肯定有 30 个没被比到。
Formal 跑通了，不代表设计没问题。 它只证明了你设的那些比对点在那些约束下是等价的。比对点之外的逻辑，工具管不着。
我曾经在一个项目里，Formal 跑了整整两周才出结果。 结果发现比对点里漏了一个关键的握手信号。两周白跑。从那以后，我每次搭环境都会先花半天时间，把比对点清单列出来，逐条 review。

⚠️ 最后提醒： Formal 环境搭建，比对点是灵魂。设错了，后面所有工作都是白费。宁可多花一天确认比对点，也不要等流片回来再后悔。

可可精品资料库