做数字验证的同行多半见过这种场景LEC跑到一半report里冒出来几个not equivalent或者Formal跑了几个小时一个property还挂在unknown上既不通过也不失败。这时候最考验人的不是工具操作而是接下来怎么判断、从哪里下手。这个系列前两篇把LEC和Formal的环境搭建、基本流程讲完了这篇PARTIII就专门聊debug。为什么单独把debug拿出来写一篇因为这两类工具的失败信息都不像仿真那样直观。仿真挂了你有一整段波形可以挨个信号查LEC和Formal给你的是一堆抽象的点状态和性质状态。命令就那么几个但同样一条报错不同人处理的时间可能差一个数量级。差别就在对原理的理解和分析的顺序上。这篇文章不打算把每个GUI按钮都讲一遍而是讲一套我反复在用的方法先分清失败类型再按链路定位最后把根因映射到设计、环境、工具三个层面。适合正在被LEC/Formal结果折磨的验证工程师也适合刚入行想建立系统debug思路的同学。1. 先搞明白LEC和Formal的debug到底在“比什么”“证什么”1.1 LEC是双镜像比对Formal是性质求证LEC的核心思路是把两个设计放在一起比较一个叫参考设计golden/reference通常是综合前的RTL一个叫实现设计implementation/revised通常是综合或布局布线后的门级网表逐点做逻辑等价性检查。它回答的问题是在同样的输入下两个设计所有关键点的输出是否一致。所以LEC的debug本质是差异分析——你要从一堆“两边的点不匹配”的现象里找出到底是设计逻辑变了、约束没对齐还是映射方式不对。Formal则完全不同它针对的是单个设计里的某些性质/断言。常见描述是给设计设定好输入约束assumption然后证明某个property在任何可达状态下都成立。它回答的不是“和谁一样不一样”而是“这个性质本身成立吗”。因此Formal debug时你面对的是两类截然不同的结果工具给出了反例说明性质被推翻或者工具做不出结论既找不到反例也证明不了。打个比方LEC像刑侦里比对两段录音是不是同一个人说的Formal像证明“只要一个盒子满足这些规则球就永远翻不出来”。前者找差异后者找反例和证明边界。很多人debug效率低就是因为没先分清楚自己处在哪种上下文里拿着一套思路到处套。1.2 读报告的顺序比读报告本身更重要我见过有人拿到结果就开GUI点开schematic开始逐根线看。我的习惯是反过来先在log里找汇总信息再决定要不要开GUI。GUI适合看局部不适合判断全局。一份LEC报告我必看四个数字matched数量、unmapped数量、aborted数量、failing数量。只要unmapped明显偏高哪怕failing只有1个我也不会急着去追那个failing点而是先处理unmapped。因为点没映射上说明两边的关键点集合本身对不上此刻的failing结果很可能是虚假失败是映射错位的副产品。Formal这边我看一个property的状态时先看它是proven、falsified还是unknown再看它是bounded还是unbounded最后看它的cone of influence规模。如果属性直接falsified先查环境约束而不是马上打开波形数周期。顺序反了debug时间大概率翻倍。2. LEC失配点定位从报告到根因的完整链路2.1 先把失败类型分清楚LEC输出里最常见的三种点状态处理思路完全不同状态含义优先排查方向not equivalent两侧逻辑确实不相等逻辑锥、约束、SVF版本unmapped参考/实现两侧找不到对应点命名映射、结构优化、blackboxaborted工具尝试过但无法完成比较运算块规模、cutpoint、引擎努力等级not equivalent是大家最敏感的但也最容易误判。很多时候它不是逻辑真不等价而是某个输入端口在比较环境里少了约束。unmapped则指向比较点集合层面的问题典型原因是综合改名、常量折叠导致寄存器消失、模块被并行替换等。aborted相对少见通常出现在超大位宽乘除法器、复杂状态机或深度嵌套时序上这时候单纯加大引擎努力不一定有用需要靠设置cutpoint或者把一个大比较切成几段。2.2 从failing list到差异锥以Synopsys Formality为例一次标准的排查链路是这样的verify之后先跑report_failing_points拿到具体层次路径用analyze_points -failing看工具自动分析的初步根因打开schematic comparison把失配点的差异锥画出来找到第一个出现逻辑分裂的节点对这个节点追问为什么它会分裂是某个输入被常数化了还是时钟域不同还是综合在两侧做了不同优化。报告里如果有类似这样的汇总我会一眼扫过去Total Reference Key Points : 1000 Total Implementation Key Points : 996 Unmatched : 0 Failing : 3关键点数量都对得上failing又有3个那就不是映射问题可以放心追逻辑锥。反过来如果Reference有1000个点Implementation只有900个那得先问那100个点去哪了。2.3 典型根因与修复策略我把这几类最常见的根因整理成了一张表每次debug前都会先对照一遍根因典型特征处理方式SVF缺失或版本不一致unmapped偏高、大量失配重新生成与本次综合完全一致的SVF文件DFT端口未约束scan_mode/scan_en悬空导致锥分裂在验证环境中将DFT端口set_constant为功能模式值时钟门控插入与时钟相关的寄存器大量失配检查时钟约束使用时钟抽象retiming导致寄存器漂移失配点都是时序点组合点正常开启sequential compare或重定时验证模式blackbox设置不一致某个macro一侧是空盒另一侧不是统一两侧blackbox列表常量优化RTL寄存器被综合为常量映射失败按需设置cutpointECO后未使用ECO模式变点之外出现奇怪失配使用ECO验证模式缩小检查范围表里的第一行值得单独说说。SVFSetup Verification File是综合工具吐出来的验证辅助文件里面记录了哪些逻辑做了哪些变换比如资源共享、datapath优化、寄存器合并。如果LEC环境里加载的SVF和网表不是同一次综合产出的工具就会对不上号产生大量虚假失败。我处理过的LEC debug case里至少有两成最终根因是SVF文件没对齐。2.4 复杂场景retiming和sequential compare普通LEC假设寄存器位置一一对应叫cycle-based comparison。但综合开了retiming之后寄存器会跨时序边界移动组合比较就会大面积报错而且报出来的点往往“左右逻辑确实不完全一样”很容易让人误以为网表出了问题。这种场景正确的做法是启动sequential compare顺序逻辑等价性检查它允许两侧寄存器位置和数量不同只比较整体时序行为。代价是运行时明显增加复杂模块可能从几分钟涨到几小时。我的建议是先用局部检查确认失配是否集中在某个模块再对这个module单独做sequential验证避免全芯片都跑在慢模式里。3. Formal debug反例和“证不出来”是两条完全不同的路3.1 拿到反例先别急着改RTL反例看起来最直观波形显示在第N拍输出错了。但在我实际遇到的case里相当高比例的“反例”是假失败根源往往不在设计本身而在property和验证环境。最常见的三个原因缺少约束。某些输入在真实环境里会被限定在一个范围但验证环境里没写assume工具就替你把所有非法输入都遍历了一遍自然能找到“反例”。属性和复位时序不匹配。reset释放后的第一个采样沿状态可能还没稳定断言就判断下去了。属性本身写错比如事件触发的条件多了一个周期延迟。所以拿到CEX的第一件事永远是把反例波形和约束清单对齐确认这个违反场景在真实系统里是否可达。不可达的反例不算反例。3.2 波形不是第一手证据我的习惯是当发现一个反例时先不追波形细节先做三件事检查反例起点状态是否可达。工具默认从复位状态出发如果你的设计启动后还需要经过配置序列那么单纯放宽初始条件可能会产生伪路径。检查CEX里所有assume是否都真正生效。有时候你写了约束但因为命名作用域或语法问题约束被工具悄悄忽略了。把反例的深度和cone of influence规模对比。如果cone太大先把无关信号从波形视图里关掉只看与property直接相关的扇入锥。用“短波形窄逻辑锥”逼近问题通常比盯着全波形看要快得多。3.3 证不动状态爆炸的拆解思路unknown和falsified是两回事。如果property在bounded深度内没失败但unbounded证明一直拿不下来那多半不是逻辑错而是状态空间太大。这时候盲目提高引擎effort往往收益有限真正有效的做法是拆把复杂的property拆成若干个辅助断言lemma用中间性质搭桥对数据通路里位宽较大的信号做case split按地址域或模式分组让每个子证明面对的状态空间更小给设计加合理的抽象或边界条件把与证明目标无关的模块替换成简化模型调整引擎和超时参数必要时对特定小模块做单独证明再把结果作为约束挂到大property上。这个思路总结起来就是不要让一个prove引擎一次性遍历整个状态空间你想办法在合适的位置“切一刀”把大任务切成几个小任务。3.4 “证明通过”也要防真空还有一类debug容易被忽略——property确实proven了但结论没有意义。比如假设里把关键场景剪掉了或者约束本身不可满足工具会给出一个“空泛通过”vacuous pass。这种通过比失败更危险因为它会给人虚假的安全感。所以每次formal证明通过我都会同时检查两个东西约束集合是不是可满足的、property的功能覆盖率有没有明显空洞。证明结果要和约束可满足性、覆盖报告一起看缺一个都不算完整结论。4. 工具链层面的debug成本脚本、日志和可复现性4.1 可复现是debug的第一原则LEC和Formal的结果依赖一堆外部条件RTL版本、综合网表版本、SVF文件、约束文件、库文件、工具版本。任何一个不一致结果就可能不可复现。我见过太多次这种情况一个人拿着failing point list去问同事同事在自己机器上一跑结果完全不一样。这不是玄学是环境没对齐。我的习惯是每次run之前先把所有输入文件的版本号固定下来脚本里主动echo出版本信息和时间戳这样log本身就构成了完整证据链。debug的第一步不是改脚本而是确认你看到的失败结果是在一个干净且可复现的环境里得到的。4.2 一开始就写好“debug友好”的脚本验证脚本不能只写run的部分还要顺手把debug时需要的信息落地。LEC里我会在脚本中输出unmapped和failing点列表到独立文本文件Formal里我会把每个property的状态、运行深度、超时时间统一汇总成一个状态文件。这些看起来是小事但当你面对几十个property、已经跑了三轮回归时一个干净的汇总文件能省下大量时间。另一个小技巧是每次run之后把本次和上次的failing点列表做diff。增量式地看问题永远比全量地看问题更容易定位。很多回归问题其实是最近一次改动引入的diff结果会直接把嫌疑范围缩小到最近改过的代码或约束。4.3 把“增量验证”变成默认动作全量重跑的成本很高尤其LEC跑到大模块的时候一次verify可能要数小时。小范围改动比如ECO之后我会尽量使用工具的增量或局部检查能力只对有变化的点和受影响的比较锥做验证。Formal也是同样的道理一个内部信号改动后先去确认它不在某些已证明属性的cone of influence里如果不在这些property不需要重跑。当然增量验证的前提是你对影响范围有判断力。没有把握的时候宁可靠一次全量回归换安全感也不要用一个被错误剪枝的结果去掩盖真问题。5. 一个典型LEC失配案例的复盘过程5.1 现象有一次跑完Formality报告显示3个点not equivalentunmapped为0。这3个点都集中在一个数据处理模块看起来非常集中不像全局性映射问题。5.2 排查链路我第一件事没有开GUI先跑了report_failing_points看到3个点分别是存储器的输出、rdata路径寄存器和FIFO状态寄存器。这3个点都和数据读取路径相关直觉上像是同一起因。接着用analyze_points跑了一遍提示与时钟门控相关。我没急着信先检查SVF版本确认和综合导出的一致排除SVF问题。然后打开schematic comparison沿着rdata寄存器D端的逻辑锥往上追发现锥顶除了正常数据通路还悬着一组端口scan_mode、scan_en这类DFT测试端口。到这里问题已经很清楚了——DFT端口没有被约束成固定值。工具在做等价性比较时把扫描测试模式也当成了正常工作模式。而门级网表在scan_mode有效时会切换成移位寄存器路径和参考RTL的功能行为当然不一样。于是这3个点全部被报成不等价。5.3 修复与回归修复方法是把DFT相关端口在LEC环境里设为固定常量明确进入功能模式再重新跑verify。这次3个点的状态全部变为pass整个模块比较干净通过。这个case的教训很通用LEC失败很多时候不是网表逻辑错了而是验证环境没对齐。如果你接手一个新综合版本第一反应永远应该是“环境和约束状态对了吗”而不是“网表是不是写错了”。DFT端口、复位信号、时钟约束这几类环境输入是LEC debug里排在最前面的嫌疑对象。6. 一个Formal“大属性证不动”的拆分案例6.1 问题描述另一个印象深刻的场景是给一个存储控制器模块证明跨周期复杂性质大致内容是“完成一次读写模式切换后后续数据输出不会错”。直接prove跑了两个小时仍是unknownbounded depth始终不够。一开始我的第一反应也是加effort、换引擎但效果有限。后来冷静下来分析这个property包含了两类逻辑一部分是控制状态机的迁移一部分是数据通路的扇出。这两类逻辑加在一起状态空间和逻辑深度同时很大证明引擎自然吃力。6.2 把大性质拆成控制路径和数据路径我把这个复杂property拆成了两条辅助断言第一条聚焦状态机证明在读写模式切换条件满足后内部控制状态必然在有限拍数内到达idle第二条聚焦数据通路证明在idle状态下收到请求后数据输出的扇出锥在若干拍内稳定。两条辅助断言单独证明都很快。第一条是典型的状态可达性问题状态机规模不大第二条虽然是数据通路但前置条件已经限定在idle状态输入空间小了很多。两条性质都通过后再回到原来那个复杂property上运行时间从之前的超时降到了十几分钟。我还做了一步case split按地址域把数据通路相关信号分组进一步减小每个子证明的状态空间。整体思路就是大任务拆成控制逻辑和数据逻辑两个子任务再分别用最合适的引擎去啃而不是让一个prove进程面对全部复杂度。6.3 收获Formal的debug经验很多时候就体现在“知道在哪里切一刀”。“切”得好的前提是对设计的行为、property的结构和证明引擎的特点都有判断。盲目加时间、加内存解决不了本质问题反而会掩盖方向。7. 值得长期坚持的debug习惯7.1 先定性再定位拿到任何失败结果先回答三个问题这是设计问题还是环境问题是逻辑问题还是约束问题是全量问题还是增量问题定性对了定位只是时间问题定性错了方向全反。我见过太多人把一个环境约束问题当成网表问题追到最后一整天才发现只是少写了一行DFT约束。7.2 用最小复现压缩问题LEC里把失配点压缩到最小逻辑锥手动比较参考侧表达式和实现侧表达式是否真不一致Formal里尝试把CEX用精简模块复现把与property无关的输入、寄存器全部删掉只保留最小可失败集合。整个过程尽量保留原始设计语义但裁剪掉所有无关分支。问题被压缩得越小根因看得越清楚。7.3 记录结论胜过记录过程我会维护一个简单的debug记录表按“现象、初步怀疑、证据、根因、修复、验证”六列填。一段时间后这张表就是自己的checklist。遇到类似报错先翻记录再查工具手册。很多工具问题在手册里写得绕来绕去真实的case记录里往往一句话就说清了。7.4 别一个人扛如果一个问题超过半天还没有方向果断停下来找人复述一遍卡点。很多debug的突破口来自另一个人随口问的一句“你确定SVF是新生成的吗”。团队里建立共享错误库、定期过一遍典型失败case比每个人各自重复踩坑效率高一截。debug能力是可以群体复用的资产。写到最后再分享一个我自己的操作习惯每次debug结束我都会把根因和解决过程写成一条短记录下次遇到类似问题直接翻有时候十分钟就搞定了。LEC和Formal工具给我们的输出本质上都只是“现象”把现象翻译成结论的能力才是值得反复打磨的东西。希望这篇PARTIII的debug思路能帮你少走一点弯路。