★ FEATURED ARTICLE 跑 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 需要三种能力同时在线第一是会读报告知道哪些点值得追、哪些点属于预期内的 dont care第二是会切证据能把一个大逻辑锥拆成若干子锥去对比或验证第三是有很强的“约束意识”因为这类工具的所有结论都建立在约束成立的前提上。约束一错要么无穷无尽地报错要么反而给你一个漂亮的 pass这才是最危险的。1.2 先把“失败类型”分清楚再动手和仿真 debug 最大的不同在于LEC/Formal 报出来的问题很少只有一种原因你如果不先分类很容易在一个假方向上浪费一整天。按我自己的经验可以把失败归成四大类环境类问题脚本设置错了、库没读全、时钟约束没给好、复位逻辑没定义。这类问题在 LEC 里最常见表现为大量 unmatched points 或者大面积 fail。约束类问题该加 constant 的地方没加该设 dont 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_pointsCadence Conformal 里对应的是report unmatch一类命令。如果 unmatch 集中在某些时钟门控单元、扫描链逻辑、测试逻辑上那大概率是正常现象。因为综合工具插入 scan chain、clock gating 之后实现设计里会多出很多参考设计没有的内部节点这部分本来就不需要匹配。但如果 unmatch 出现在普通功能寄存器或者输出端口上就要高度怀疑是环境设置问题比如某个时钟域没有被正确声明、某个常量没设置好。到了 verify 阶段工具真正开始比较匹配点的逻辑锥。这时的核心输出是 failing point 列表。Formality 里通常用report_failing_pointsConformal 里是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 设置仅扫描链相关路径 failscan_enable 没有设为 constant在 LEC 环境中 set_constant scan_enable 0时钟门控单元 mismatch门控逻辑被工具重排检查 merge_clock_gating 与 dont touch 属性输出端口 fail输出端存在组合逻辑未匹配用 logic cone 查看输出端分支只有 ECO 区域 failECO cell 连接错误核对 ECO 前后网表 diff重点看电源域和隔离单元异步复位路径 fail异步复位树不一致检查异步复位同步器层次这些模式看起来简单但每个底下都有坑。比如 scan_enable 的问题如果设计里同时存在 scan 和 functional 两套模式你只设了其中一个工具会默认另一个是自由变量。这样 scan 模式下的逻辑也会参与比较就会产生一堆看起来莫名其妙的 fail。解决方法是把所有测试模式信号全部定死LEC 环境只用来验证功能逻辑测试模式逻辑不应该出现在等价性比较里。2.4 修 LEC fail 的正确顺序一旦定位到真正的逻辑差异点修复顺序要有讲究。首先如果问题出在综合脚本或环境约束优先修正环境不要动 RTL。很多团队喜欢通过修改 RTL 去“哄”LEC 过关但 RTL 一旦为了迁就网表而改别扭后面 Formal 跑起来会更痛苦。其次如果问题出在网表实现方式不同但功能上确实等价那应该通过设置 proper constants、dont care、或者工具允许的 ignore/cut 机制去排除而不是强行改 RTL。比如某些不定态X态优化工具认为 sequencer 里未初始化位应该按 dont care 处理实际综合也按 dont care 优化了这时候给工具足够的信息比改 RTL 更合理。最后只有当双方逻辑函数真的不等价且环境约束完全正确时才回到 RTL 去修 bug。这个 bug 可能出现在参考设计里也可能出现在实现设计里不要想当然地认为是前一个版本写错了。我曾经碰上过参考设计里一个 history 版本漏了 pending flag 更新而新网表反而修对了LEC 报 fail 后所有人都在网表里找问题最后发现是参考 RTL 有 bug。所以在 debug 时永远保持“两边都有可能错”的怀疑态度。3. Formal 专项看懂反例和证明引擎3.1 先确认 cex 是不是真实的Formal property verification 跑挂之后工具通常会给出一个 counter-exampleJasperGold 和 VC Formal 里都能以波形形式打开。很多人看到 CEX 波形就直接去追 RTL bug但更稳妥的做法是先问三件事这个反例的激励序列是否违反了设定的 constraint这个反例的初始状态是否从真实的可复位状态出发这个反例在现实中是否真的能被外部输入驱动出来第一个问题最容易被忽略。比如你写了一条 assumptionassume 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 boxFormal 里可能把某些存储单元或第三方 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 设置后重跑 matchLEC 一个点反复 fail逻辑锥中某个分支有差异打开 logic cone逐层对比分支信号LEC fail 随综合版本变化综合选项或 DFT 插入策略变化对比综合脚本选项重点看 scan/clock gatingFormal 反例违反 assumptionconstraint 未覆盖初始状态检查 reset 序列和 initial block 约束Formal 反例过长且单调重复状态空间存在大计数/大比较逻辑拆模块或增加 abstraction/cut pointFormal 属性 proven 但仿真不满足约束定义了过强条件检查 assert 是否是“真成立”还是“伪成立”Formal 一直 abort引擎不收敛或设计有乘法器/大位宽换引擎、加辅助不变量或拆分子属性LEC/Formal 全部 pass但仿真有 bug环境约束屏蔽了错误路径重新审视约束是否过强检查 vacuous pass这张表不能代替深入分析但它能让你的第一步判断不至于跑偏。工具报出来的东西往往比想象中更“诚实”很少无中生有更多时候是环境和约束给错了。4.4 什么时候该找工具支持什么时候该自己扛很多工程师遇到 abort 或者奇怪反例第一反应是提 case 给工具 vendors这个习惯有价值但要在自己排查过一轮之后再做。一个合格的 debug 工程师应该在提 case 前把下面这些信息准备好最小复现用例、当前约束文件、设计版本、运行日志、你已经做过的分析结论。如果连“问题出在约束还是 RTL”都没搞清楚就提 casevendor 也只能干瞪眼。反过来如果你已经在逻辑锥里把某个模块单独提出来验证过确认约束没问题但工具仍报出明显不可能的反例那很值得向工具厂商反馈。工具确实存在 bug但概率远低于约束 bug。不要一上来就“甩锅”给工具这会拖慢项目进度也不利于你个人 debug 能力的成长。5. 让 LEC/FORMAL debug 收敛的几条工程经验5.1 建立“最小复现用例”的习惯无论是 LEC 还是 Formal一旦出现难缠的 failure我的第一步永远是尝试构造最小复现用例。把所有和失败无关的模块、信号、约束全部剥离只留下能触发问题的那一小段逻辑。这个动作听起来费时间但它能带来三个巨大收益一是让工具跑得更快迭代更短二是帮你确认问题本质三是可以安心地把最小用例交给同事或工具 vendor让大家都在一个“不喘气”的环境里讨论。构造最小用例也有一些基本功。LEC 里可以先从完整网表中裁出一个子模块再对子模块单独跑 compareFormal 里可以新建一个 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 其实就已经完成一半了。祝一次过少踩坑。
阅读完成 · 觉得有帮助？
是什么？原理、场景与加载失败排查全解析)
