跑 LEC 和 Formal 验证，最让人头疼的不是 setup、不是跑命令，而是 debug。很多团队把这两类检查当成流片前的一道例行关卡，跑过了就签字，跑挂了就找工具供应商丢 log。但当设计规模上来、ECO 一多、跨时钟域的约束链变复杂之后，debug 才是整个流程里最耗人力的部分。它不像仿真那样拉一条信号波形追到根因，而是要面对一整套“逻辑证据”：一堆 failing points、一个 counter-example、一片 aborted 或者 unmatched 的列表。你得学会把这些工具输出翻译成真实的设计问题，再决定是改 RTL、改约束，还是改验证环境本身。这篇是 LEC/FORMAL 系列的第三篇，主题只有一个：debug。
系列的前两篇分别讲了 LEC 和 Formal 验证的基本原理、工程化落地方法，包括流程怎么搭、约束怎么写、任务怎么拆分、哪些场景适合 equivalence check、哪些场景适合 property verification。但很多读者反馈，最缺的还是“跑挂了之后怎么办”的这部分。这篇就拿这个当主线。我会把 LEC 和 Formal 分开讲，因为两者的 debug 思路虽然同源，工具界面和证据形式却完全不同；混在一起讲，只会越看越乱。另外，文章里提到的命令以 Synopsys Formality、Cadence Conformal、JasperGold/VC Formal 这类常见工具为主，但方法对其它工具同样适用。
1. 先把 debug 的正确姿势建立起来
1.1 你调试的其实是一台“证明引擎”
刚接触 LEC/Formal 的人最容易犯的一个错误，是把它当成“另一种仿真器”。仿真器给你的是时序波形，你按照时钟沿和前级信号一层层往回找，早晚能找到源头；但 LEC/Formal 工具给你的是“证据”：Formal 引擎会告诉你某个属性为什么能被违反，LEC 引擎会告诉你两个设计在哪个逻辑锥上不等价，但它不会像仿真那样把完整波形按时间轴摆在你面前。
这里有个很关键的心态转变：你面对的不是一个“执行过程”，而是一个“逻辑系统”的求解结果。在 LEC 里，工具把参考设计和实现设计各自映射成布尔逻辑网络，然后比较每个关键点的逻辑锥；在 Formal 验证里，工具把 RTL 转成状态转移系统，再通过 SAT、BDD 或者插值算法去探索状态空间。换句话说，debug 的第一步不是“找信号”，而是“看懂工具到底证明了什么、没有证明什么”。如果工具证明了一个反例存在，那这个反例背后一定有一套输入序列或者初始状态组合；如果工具只是 report aborted，那可能不是设计错了，而是问题太难解、证明路径被某种结构卡住了。
我个人的看法是，LEC/Formal debug 需要三种能力同时在线：第一是会读报告，知道哪些点值得追、哪些点属于预期内的 don't care；第二是会切证据，能把一个大逻辑锥拆成若干子锥去对比或验证；第三是有很强的“约束意识”，因为这类工具的所有结论都建立在约束成立的前提上。约束一错，要么无穷无尽地报错，要么反而给你一个漂亮的 pass，这才是最危险的。
1.2 先把“失败类型”分清楚再动手
和仿真 debug 最大的不同在于，LEC/Formal 报出来的问题很少只有一种原因，你如果不先分类，很容易在一个假方向上浪费一整天。按我自己的经验，可以把失败归成四大类：
- 环境类问题：脚本设置错了、库没读全、时钟约束没给好、复位逻辑没定义。这类问题在 LEC 里最常见，表现为大量 unmatched points 或者大面积 fail。
- 约束类问题：该加 constant 的地方没加，该设 don't care 的地方没设，formal 的 assumption 和真实场景不一致。工具不是在“撒谎”，它只是严格按你给的输入空间在证明。
- 设计类问题：RTL 和网表之间真的有功能差异，或者 Formal 断言对应的 RTL 行为确实有 bug。这类问题最老实，修起来也最明确。
- 抽象/表达类问题：两个设计在结构上不等价，但功能上等价；或者断言写得本身不合理，导致 vacuous pass 或者 impossible-to-cover 的怪异结果。
我在实际项目里见过太多次“看起来像设计 bug，其实是一句约束写错”的情况。不夸张地说，LEC/Formal debug 里，环境类和约束类问题加起来能占到一半以上。所以拿到第一次 failure report，先别急着打开 RTL 开始找 bug，先把失败类型归类，再去动 RTL，这才是高效流程。
2. LEC 专项：从 mismatch 到根因的定位套路
2.1 先读 unmatch，再看 failing points
正规的 LEC 流程大概是这样：准备参考设计和实现设计、读入库、link、设置约束、match、verify。这里的 match 阶段会把参考设计和实现设计里的寄存器、输出端口等关键点做一一对应；如果对应不上，就是 unmatched points。很多团队一看 unmatch 数量大就慌，其实 unmatch 本身不一定是功能错误。
以 Synopsys Formality 为例，跑完 match 之后可以执行report_unmatched_points，Cadence Conformal 里对应的是report unmatch一类命令。如果 unmatch 集中在某些时钟门控单元、扫描链逻辑、测试逻辑上，那大概率是正常现象。因为综合工具插入 scan chain、clock gating 之后，实现设计里会多出很多参考设计没有的内部节点，这部分本来就不需要匹配。但如果 unmatch 出现在普通功能寄存器或者输出端口上，就要高度怀疑是环境设置问题，比如某个时钟域没有被正确声明、某个常量没设置好。
到了 verify 阶段，工具真正开始比较匹配点的逻辑锥。这时的核心输出是 failing point 列表。Formality 里通常用report_failing_points，Conformal 里是report compare data或者直接看 GUI 里的 failing 表格。拿到列表之后，先按扇出排序或者按层次路径排序，看看失败点是集中在某一个模块，还是分散在全芯片。集中式失败往往意味着局部逻辑差异；分散式失败则更可能是顶层约束或者全局配置错误。
2.2 用逻辑锥视图追根因，而不是靠肉眼扫 RTL
很多新人第一次看到 failing points 报告，第一反应是打开两个版本的 RTL，用文本 diff 工具比对。如果版本差异很大，比如 ECO 之后插了很多 ECO cell，这个做法基本无效。正确姿势是用工具自带的逻辑锥分析功能。
Formality、Conformal 都提供 schematic / logic cone 视图，可以把某个 failing point 的完整逻辑锥画出来，参考设计和实现设计并排对比。你不需要从输入到输出推一遍，而是要关注“从哪个节点开始，两边的逻辑函数出现不同”。这个起点往往就是根因所在。比如一根信号在参考设计里来自某个 always 块，在实现设计里被 DFT 逻辑绕了一下，如果这个 DFT signal 没有正确设置成 constant，就会导致关键点 fail。
我自己的习惯是：先看 fail point 的前一级或者前两级，如果两边结构看起来一致，就把注意力放到更早期分支点，比如时钟门控、异步复位、多路选择器的 select 信号。工具一般允许你直接 “focus” 到某个节点，并按扇出方向追踪。在 Conformal 里我常用add_cut_point和add_ignore_point来切分逻辑锥，但这属于后手手段；在没有完全确认失败原因之前，不建议用 cut point 去“绕过”问题，否则容易掩盖真实差异。
2.3 常见 LEC 失配场景与对应解法
从实际项目看，LEC 失配的原因其实很有限，主要集中在几个固定模式上。我列成一张表，方便你对照：
| 症状 | 常见原因 | 优先排查方向 |
|---|---|---|
| 大量寄存器级 failing | 时钟或复位约束不完整 | 检查 all_clocks、all_resets 设置 |
| 仅扫描链相关路径 fail | scan_enable 没有设为 constant | 在 LEC 环境中 set_constant scan_enable 0 |
| 时钟门控单元 mismatch | 门控逻辑被工具重排 | 检查 merge_clock_gating 与 don't touch 属性 |
| 输出端口 fail | 输出端存在组合逻辑未匹配 | 用 logic cone 查看输出端分支 |
| 只有 ECO 区域 fail | ECO cell 连接错误 | 核对 ECO 前后网表 diff，重点看电源域和隔离单元 |
| 异步复位路径 fail | 异步复位树不一致 | 检查异步复位同步器层次 |
这些模式看起来简单，但每个底下都有坑。比如 scan_enable 的问题，如果设计里同时存在 scan 和 functional 两套模式，你只设了其中一个，工具会默认另一个是自由变量。这样 scan 模式下的逻辑也会参与比较，就会产生一堆看起来莫名其妙的 fail。解决方法是把所有测试模式信号全部定死，LEC 环境只用来验证功能逻辑，测试模式逻辑不应该出现在等价性比较里。
2.4 修 LEC fail 的正确顺序
一旦定位到真正的逻辑差异点，修复顺序要有讲究。首先，如果问题出在综合脚本或环境约束，优先修正环境，不要动 RTL。很多团队喜欢通过修改 RTL 去“哄”LEC 过关，但 RTL 一旦为了迁就网表而改别扭，后面 Formal 跑起来会更痛苦。
其次，如果问题出在网表实现方式不同，但功能上确实等价，那应该通过设置 proper constants、don't care、或者工具允许的 ignore/cut 机制去排除，而不是强行改 RTL。比如某些不定态（X态）优化，工具认为 sequencer 里未初始化位应该按 don't care 处理，实际综合也按 don't care 优化了；这时候给工具足够的信息，比改 RTL 更合理。
最后，只有当双方逻辑函数真的不等价，且环境约束完全正确时，才回到 RTL 去修 bug。这个 bug 可能出现在参考设计里，也可能出现在实现设计里，不要想当然地认为是前一个版本写错了。我曾经碰上过参考设计里一个 history 版本漏了 pending flag 更新，而新网表反而修对了，LEC 报 fail 后所有人都在网表里找问题，最后发现是参考 RTL 有 bug。所以在 debug 时，永远保持“两边都有可能错”的怀疑态度。
3. Formal 专项：看懂反例和证明引擎
3.1 先确认 cex 是不是真实的
Formal property verification 跑挂之后，工具通常会给出一个 counter-example，JasperGold 和 VC Formal 里都能以波形形式打开。很多人看到 CEX 波形就直接去追 RTL bug，但更稳妥的做法是先问三件事：
- 这个反例的激励序列，是否违反了设定的 constraint？
- 这个反例的初始状态，是否从真实的可复位状态出发？
- 这个反例在现实中，是否真的能被外部输入驱动出来？
第一个问题最容易被忽略。比如你写了一条 assumption：assume property (a |=> b);，但 Formal 引擎在产生 CEX 时却从某个非法状态启动，绕过了第一条 assumption 的时序约束。然后工具交出的反例看起来就“不真实”。遇到这种情况，优先检查 constraint 的作用域和 initial state 约束。在 SVA 里，reset 通常用disable iff处理，但 initial 状态如果是 X态，则很容易产生奇葩 CEX。
第二个问题同样关键。很多 RTL 在复位后需要若干周期的初始化序列，比如 FIFO 指针清零、校准模块启动。如果 Formal 环境没有把这个初始化序列建模成 constraint，工具可能从“理论上能到达但实际永远到不了”的状态开始，给出一个不可复现的反例。
第三个问题则涉及“环境真实性”。形式验证的输入空间是无限的，但真实使用场景会限制很多输入的组合。假设一个总线协议模块，它的地址信号在实际系统中只有几种合法组合，但你在 Formal 环境里没有加对应 constraint，那工具就可能在非法地址组合上给你报反例。这不代表 RTL 一定是错的，而是说明约束不完整。遇到这种情况，应该加强环境建模，而不是急着改设计。
3.2 用 cover property 判断是不是“伪命题”
另一种很常见的 Formal debug 场景是：一条 assertion 报 fail，但它的 CEX 路径非常短，甚至在代码 review 时你会觉得“这怎么可能走到”。这种情况我通常先写一条 cover property，专门去覆盖那条 assert 的前置条件，看看这个前置条件到底能不能被满足。
举例来说，如果 assert 一个 FIFO full 后不能再写，工具报了一个“full 之后又有 write”的反例。你先写cover property (fifo_full && write_en);，如果 cover 根本 cover 不到，那就是断言本身的前置状态不可达，问题出在“状态不可达”上，而不是写保护逻辑真的失效。如果 cover 能 cover 到，再回头去看那个 CEX，问题就清楚多了。
cover 和 assert 的关系在 Formal debug 里非常强大。它能帮你快速区分“设计真的错”和“断言写得不可达”两类问题。很多工程师因为省事，跳过 cover 直接分析 CEX，结果在不可达状态上绕了半天。记住：Formal 工具只会告诉你“在这个状态空间里”，从不说“在这个真实系统里”。覆盖率的分析，就是帮你判断状态空间是否符合真实系统的桥梁。
3.3 深入 debug 长反例和 abort
除了直接报 fail 的情况，Formal 验证里还经常遇到 aborted 或者 bounded proof。很多设计在 BMC 深度 20 cycle 以内能证明属性，深度一旦超过 80 cycle 就 abort。这时你面对的不是 design bug，而是“引擎无法在给定时间内证明属性”。
对于这种问题，debug 的核心是“缩短证明路径”或“降低状态空间复杂度”。常见手段包括：
- 用
assume和constraint收敛输入范围，把合法输入空间缩小，减少 SAT 求解难度。 - 把一个大模块拆分成几个小模块分别验证，拆分后每个属性只依赖局部信号。
- 使用 cut point 抽象，把不影响目标属性的内部信号做抽象处理。
- 检查是否存在某些组合逻辑爆炸点，比如大位宽加法器、乘累加单元，必要时单独建模或增加抽象。
这里要特别提醒一下，不要一遇到 abort 就无脑提高资源上限、加大 depth。很多 abort 是因为设计里存在“无界循环”，比如一个计数器可以在任意时刻被加载成任意值，这会导致状态空间急剧膨胀。你应该先排查是否存在这类“类自由变量”的输入，通过合理约束来剪枝，而不是靠蛮力去证明。
3.4 反例波形的定位技巧：追“token”而不是追“信号”
Formal 的 CEX 和仿真波形有一个本质区别：Formal 的 CEX 往往是从一个非法初始状态或者一个特殊约束漏洞里长出来的，它的时序路径可能只有十几个周期，但这十几个周期里每个信号都经过复杂的组合变换。追信号经常追到一半就绕晕了。
我比较推荐的方法是“追 token”：在一个 CEX 里，找到第一个偏离期望行为的点，比如某个 flag 第一次被置高、某个计数器第一次跳到异常值，然后沿着这个“关键事件”作为 token 往前追。比如断言是“当 a 发生之后，b 必须在 5 拍内拉高”，CEX 显示 b 没拉高。这时不要从 a 拉高开始慢慢看，而是直接在 b 的赋值逻辑上找“为什么这个周期没有拉高”。如果是某个中间信号复位值不对，就再往前看那个中间信号的置位条件。
这个思路和软件 debug 里的二分法很像，只是形式验证里信号扇出更宽、组合逻辑更深，更讲究直接跳到异常点分析。配合工具自带的“focus on driver”功能，一般几个来回就能定位到根因。
3.5 工具引擎的选择对 debug 效率影响很大
同样一条属性，用 BMC 和用 induction 去证，得到的反馈完全不一样。BMC 只能告诉你“在这几个周期内是否存在反例”，深度不够时什么都证明不了；induction 能做 unbounded proof，但对 RTL 的可证明性要求更高。JasperGold 和 VC Formal 一般会自动调度多个 engine，但作为 debug 的人，你需要关注调度日志。
如果属性卡住不收敛，可以尝试把 engine 显式切为某种更适合的算法。比如 RTL 里有大量算术逻辑时，SAT-based 引擎往往比不上 word-level 或者 BDD 风格的引擎；如果是深层状态机，适合用 induction 加辅助不变量。还有一种实用做法是，先把属性放到一个简单约束的子模块上跑通，再逐步放开约束，这样能更快判断是引擎算法问题还是设计结构问题。直接在一个复杂的全模块上启动多种引擎协同证明，虽然理论上很好，但 debug 时反而不好定位。
4. 两个流程共通的“高频坑”与排查速查
4.1 别让“黑盒”把你带到沟里
LEC 和 Formal debug 都经常用到黑盒化处理。LEC 里可能把某些模拟宏、PLL、SRAM 设成 black box，Formal 里可能把某些存储单元或第三方 IP 抽象掉。但黑盒一旦设错，后面所有结果都会跟着错。
我见过最典型的坑是：Formal 环境里把某个 FIFO 设成 black box，结果忽略了这个 FIFO 内部有读写冲突保护逻辑，而断言恰好在验证读写冲突。工具以为 FIFO 始终可以同时读和写，于是给出反例。这个反例本质上是因为黑盒覆盖掉了真实行为，不是设计 bug。所以无论 LEC 还是 Formal，当你开始怀疑反例“太假”的时候，第一时间去检查所有黑盒/抽象组件，确认它们没有掩盖关键逻辑。
4.2 版本、日志、环境记录：debug 的“三件套”
这条经验是从无数次返工里得来的：任何一次 LEC 或 Formal 运行，都要完整记录设计版本、工具版本、约束文件版本、运行命令、关键 report 的摘要。最好能生成一个 debug 归档目录，按日期命名，把每次修改前后的 log 对比保留下来。
如果不做版本记录，你很可能陷入“改了 RTL，重跑，失败点变了，但不知道哪个改动导致的”这种泥潭。形式验证工具的运行时间长，一次 full proof 可能跑好几个小时；如果环境不干净，一次 debug 循环就能耗掉大半天。建议每个迭代只改一个变量，并且把改动前后 report 里 failed/unmatched/aborted 的数量变化记下来。这个习惯看起来不起眼，实际上能帮你把 debug 效率提升一倍以上。
4.3 症状到根因的快速速查表
结合 LEC 和 Formal 的调试经验，我整理了一份高频问题速查表，适合在拿到新 failure 时先用它做初筛：
| 症状 | 大概率方向 | 第一步动作 |
|---|---|---|
| LEC 大面积 unmatch | 时钟/复位/常量约束缺失 | 补全时钟域和 constant 设置后重跑 match |
| LEC 一个点反复 fail | 逻辑锥中某个分支有差异 | 打开 logic cone，逐层对比分支信号 |
| LEC fail 随综合版本变化 | 综合选项或 DFT 插入策略变化 | 对比综合脚本选项，重点看 scan/clock gating |
| Formal 反例违反 assumption | constraint 未覆盖初始状态 | 检查 reset 序列和 initial block 约束 |
| Formal 反例过长且单调重复 | 状态空间存在大计数/大比较逻辑 | 拆模块，或增加 abstraction/cut point |
| Formal 属性 proven 但仿真不满足 | 约束定义了过强条件 | 检查 assert 是否是“真成立”还是“伪成立” |
| Formal 一直 abort | 引擎不收敛或设计有乘法器/大位宽 | 换引擎、加辅助不变量或拆分子属性 |
| LEC/Formal 全部 pass，但仿真有 bug | 环境约束屏蔽了错误路径 | 重新审视约束是否过强，检查 vacuous pass |
这张表不能代替深入分析，但它能让你的第一步判断不至于跑偏。工具报出来的东西往往比想象中更“诚实”，很少无中生有，更多时候是环境和约束给错了。
4.4 什么时候该找工具支持，什么时候该自己扛
很多工程师遇到 abort 或者奇怪反例，第一反应是提 case 给工具 vendors，这个习惯有价值，但要在自己排查过一轮之后再做。一个合格的 debug 工程师，应该在提 case 前把下面这些信息准备好：最小复现用例、当前约束文件、设计版本、运行日志、你已经做过的分析结论。
如果连“问题出在约束还是 RTL”都没搞清楚就提 case，vendor 也只能干瞪眼。反过来，如果你已经在逻辑锥里把某个模块单独提出来验证过，确认约束没问题，但工具仍报出明显不可能的反例，那很值得向工具厂商反馈。工具确实存在 bug，但概率远低于约束 bug。不要一上来就“甩锅”给工具，这会拖慢项目进度，也不利于你个人 debug 能力的成长。
5. 让 LEC/FORMAL debug 收敛的几条工程经验
5.1 建立“最小复现用例”的习惯
无论是 LEC 还是 Formal，一旦出现难缠的 failure，我的第一步永远是尝试构造最小复现用例。把所有和失败无关的模块、信号、约束全部剥离，只留下能触发问题的那一小段逻辑。这个动作听起来费时间，但它能带来三个巨大收益：一是让工具跑得更快，迭代更短；二是帮你确认问题本质；三是可以安心地把最小用例交给同事或工具 vendor，让大家都在一个“不喘气”的环境里讨论。
构造最小用例也有一些基本功。LEC 里可以先从完整网表中裁出一个子模块，再对子模块单独跑 compare；Formal 里可以新建一个 top wrapper，只实例化出错模块，并直接把接口信号用 constraint 钉死。这个 wrapper 里不要引入任何真实系统中的其它子模块，防止干扰。等到最小用例能稳定复现失败，再逐步加回约束，找到“临界约束变化点”。
5.2 约束文件写“注释版”，不要只写命令
这一点我在前两篇里提过，但 debug 场景下更值得强调。在扫描 constraint 文件排查问题时，一份注释清晰的约束文件就是你的地图。每个 assumption 都要注明来源，比如来自 datapath 的握手协议，还是来自总线规约；每条 constant 设置都要说明是哪个测试模式下的要求。没有注释的约束，三个月后你自己都看不懂，更别说快速 debug。
我在做 Formal 验证时，习惯把约束分成三段：复位/初始化段、输入协议段、环境边界段。复位段里写清复位信号、有效电平和释放条件；协议段写清握手、超时、合法组合；环境边界段写清地址范围、数据宽度和位宽限制。LEC 的 constant 设置也单独放一个文件，专门维护 scan_enable、test_mode、power_switch 这类测试相关信号。这样每次 debug 都可以快速定位到“该看哪段约束”。
5.3 团队协作：debug 文档要跟着 case 走
大型芯片项目里，一次 LEC/Formal debug 往往不是一个人能独立完成的。前面有架构师确认协议，中间有 RTL 工程师看代码，后端有综合工程师看网表。如果每个人只在口头或者群里沟通，信息很快就会丢。我们团队的做法是给每个失败 case 建一个 debug 页面，按时间顺序记录：问题现象、初步判断、验证动作、结论。别人接手时，不需要重新走一遍你的思考路径。
这个文档里我还会放上“已排除项”，把已经确认没问题的方向和原因写清楚。很多时候 debug 效率低不是因为没有思路，而是因为反复在同一个错误方向上打转。有了已排除项的记录，后续的人就能直接跳过这些雷区。
5.4 一个容易忽略的终点：回归与防回归
最后想强调一点，LEC/Formal debug 结束之后，不要只验证当前这个失败点，一定要跑一轮回归。因为你的修改可能让之前的 pass 变成 fail。比如你在 Formal 环境里加了一个 assumption，它确实解决了一个反例，但这个 assumption 也可能把另一个本应验证的合法行为给堵死了，导致变成 vacuous pass。不做回归，这个问题要等到下个版本才暴露。
LEC 改完约束或者 RTL 之后，也要重新跑整芯片的 compare，不能只重新跑刚才的 module。回归范围可以分层：先跑当前模块，再跑包含该模块的上层，最后做全芯片。虽然消耗时间，但能有效防止“修一处坏一片”的情况。
这套 debug 的方法论，没有一个是高深理论，都是实打实从项目里磨出来的。对我来说，最核心的一点是：看到失败报告不要焦虑，更不要急着去“改点什么”。先把失败分类，把证据看明白，把最小复现做出来，再动第一刀。很多问题其实在分类和复现阶段就已经暴露了，根本不需要陷入漫长的逻辑分析。
如果你现在正卡在一个 LEC/Formal 的 failure 上，强烈建议先停下手，按这篇文章的框架把报告拆一遍。当你把问题归到“约束问题”还是“设计问题”这两个篮子里的那一刻，debug 其实就已经完成一半了。祝一次过，少踩坑。
