1. 形式验证卡在常值问题上的排查思路做数字后端或者逻辑综合的朋友对形式验证工具报出大量失败点这件事应该都不陌生。尤其是跑完综合、插入扫描链、或者做完时钟树之后拿网表和参考设计做等价性检查工具突然告诉你几百上千个比较点不匹配这时候最怕的就是一头扎进波形里逐个比对。实际上相当一部分失败并不是真正的逻辑错误而是常值问题在作祟——工具认为某个信号应该是恒定值但另一侧却认为它可以翻转或者两边对同一个信号给出的常值方向相反。这类问题在形式验证里非常典型排查起来有章可循。这篇内容围绕“几个常值问题导致形式验证失败”的排查方法展开把我在实际项目里反复遇到的几类常值失配场景拆开讲清楚。核心关键词包括形式验证、常值传播、等价性检查、约束一致性、扫描链插入、优化边界。适合正在做综合后验证、扫描链插入后验证、或者 ECO 之后回归验证的工程师参考也适合刚接触形式验证、看到满屏失败点不知道从哪下手的新人。我会从常值问题为什么会产生讲起一直讲到具体怎么定位、怎么修、怎么避免下次再踩。先说清楚一个基本认知形式验证工具做等价性检查时并不是简单地逐门比对而是基于比较点做逻辑锥的匹配和求解。工具会在两侧设计里寻找对应的关键点比如寄存器输出、输出端口然后证明两侧在相同输入激励和相同约束下行为一致。常值问题之所以致命是因为一旦工具判定某个信号在参考侧是常数 0而在实现侧是可变的那么从这个信号出发的所有下游比较点都会连带失败。一个常值失配可能放大成几十上百个失败点这就是为什么很多人看到失败数量巨大就慌了其实根因可能只有一两个。提示看到失败点数量异常多的时候先别急着看单个比较点的波形优先怀疑常值失配和约束不一致这两类全局性问题它们的失败传播特征就是“一倒一大片”。2. 常值问题到底从哪来五类高频成因拆解2.1 综合优化把“看似可变”的信号钉成了常数最常见的一类是综合工具在优化阶段做了常值传播。参考设计通常是 RTL里某个信号在功能上确实可能翻转但由于上游某个配置寄存器被约束成了固定值或者某个模式选择信号在综合时被 tie 死综合工具就会把这个信号一路传播成常数然后在实现侧把它优化掉。等到形式验证时参考侧还是原始的 RTL 行为实现侧已经是优化后的网表工具一比对就发现参考侧这个信号能变实现侧是常数失配。这里的关键在于综合工具做常值传播是合法且必要的优化它没有错错的是验证环境没有把综合时的假设同步给形式验证工具。比如综合脚本里对某个 test_mode 信号设了set_case_analysis 0那形式验证的约束文件里也必须体现同样的假设否则工具就会按“该信号可变”去求解自然对不上。我踩过的一个典型坑某项目综合时为了面积把一组始终为 0 的配置位优化掉了验证时忘了在约束里把这些配置位固定结果工具认为这些位可以取任意值下游一大片逻辑全部失配。后来在约束文件里补上对应的 case analysis失败点瞬间从几百个降到个位数。2.2 扫描链插入改变了寄存器的可控性扫描链插入是常值问题的另一个重灾区。插入扫描之后原本普通的触发器变成了带扫描多路器的结构扫描使能信号scan_enable在功能模式下应该为 0但在验证时如果约束没设对工具会认为 scan_enable 可以自由翻转于是所有触发器在扫描模式下都变得“可控”逻辑锥的求解空间被急剧放大常值关系被打破。更隐蔽的一种情况是扫描链插入过程中对某些常量寄存器做了替换。比如原本 tie 到 0 的寄存器被替换成了扫描触发器虽然功能上仍然输出 0但工具在结构比对时可能识别不出这种等价关系从而报出常值失配。这类问题需要结合扫描链的插入报告和形式验证的匹配报告一起看确认哪些寄存器被替换、替换后功能是否真的等价。2.3 时钟门控与使能信号的常值假设不一致时钟门控单元ICG的插入也会引入常值问题。综合或后端阶段插入 ICG 时往往会给门控使能信号加上特定的常值假设比如某个 always-on 的使能信号被认定恒为 1。如果形式验证时没有同步这个假设工具会认为使能可以变门控时钟的行为就和参考侧对不上进而导致下游所有由该时钟驱动的寄存器比较点失败。这类问题的排查要点是先确认时钟门控的使能信号在两侧的常值状态是否一致再看门控单元本身的使能逻辑是否被正确建模。很多时候失败点集中在某个时钟域基本就能锁定是该时钟域的门控假设出了问题。2.4 黑盒与不关心区域的常值处理差异设计里如果有黑盒比如模拟 IP、存储器模型形式验证工具对黑盒输出的处理方式会直接影响常值判定。参考侧黑盒输出可能被建模成自由变量实现侧如果对黑盒输出做了常值假设或者接了固定值两边就不一致。同样不关心dont care区域的处理也容易出问题综合时把 dont care 优化成了某个常值验证时工具却按自由变量处理失配就来了。处理这类问题的原则是黑盒的建模方式在两侧必须统一dont care 的优化结果要么在约束里显式声明要么在验证时用工具的不关心处理选项对齐。别指望工具自动猜对你的意图该写的约束一个都不能省。2.5 复位与初始化状态的常值分歧复位逻辑是常值问题的第五个高频来源。参考设计里某个寄存器复位后是 0实现侧如果因为优化或者扫描替换导致复位值变了或者复位信号本身的极性、有效条件在两侧建模不一致工具就会在初始化状态上产生分歧。这类失配的特征是失败点往往集中在复位释放前后的时间窗口或者集中在带复位的寄存器上。排查时先看复位信号的约束是否两侧一致再看复位值是否在优化过程中被改动。有些工具支持指定初始状态如果参考侧和实现侧的初始状态假设不同也会表现为常值失配。3. 定位常值失配的实操流程3.1 第一步从失败报告里提取常值线索拿到形式验证的失败报告后不要急着看第一个失败点。先做一件事统计失败点的分布。按模块、按时钟域、按信号类型分类看失败是否集中在某个区域。如果失败点高度集中大概率是某个上游常值信号失配导致的传播如果失败点分散才需要考虑多个独立问题。大多数形式验证工具的报告里会标注失败原因类型常值失配通常会有类似“constant mismatch”“constant conflict”的标记。把这些标记的失败点单独筛出来看它们共同的上游信号是什么。工具一般也提供诊断命令能反推是哪个信号导致了常值冲突这个信息比逐个看波形高效得多。3.2 第二步用约束对齐消除假性失配筛出常值相关的失败点后第一反应应该是检查约束文件。把综合、扫描插入、时钟门控阶段用到的所有常值假设列出来逐条和形式验证的约束比对。常见的遗漏包括case analysis 没同步、scan_enable 没固定、门控使能没约束、黑盒输出没建模。这一步的经验是宁可约束写多不要写少。约束写多了工具求解空间变小可能漏掉真问题但至少不会产生假性失配约束写少了假性失配一大堆真问题反而被淹没。当然约束也不能乱写每一条都要有依据能对应到综合或后端阶段的实际假设。下面是一个约束对齐的检查清单可以照着过一遍检查项参考侧应有约束实现侧应有约束常见遗漏模式选择信号case analysis 固定值同参考侧综合脚本有、验证没写扫描使能功能模式固定 0同参考侧扫描插入后忘加时钟门控使能always-on 固定 1同参考侧门控插入报告没同步黑盒输出自由变量或固定模型与参考侧一致两侧建模方式不同复位信号极性、有效条件明确与参考侧一致复位值被优化改动配置寄存器按实际配置固定同参考侧配置位被优化掉3.3 第三步用逻辑锥回溯锁定根因信号约束对齐之后如果还有常值失配就需要做逻辑锥回溯了。方法是从失败比较点出发沿着扇入方向逐级回溯找到第一个两侧常值状态不一致的信号。这个信号就是根因它下游的所有失配都是它传播出来的。回溯时有个技巧优先看那些被优化掉或者被替换的信号。综合优化掉的信号、扫描替换的寄存器、门控插入改变的使能路径这三类是常值分歧的高发区。工具一般提供扇入追踪和匹配点报告结合这两份报告能快速定位到分歧点。我通常的做法是先在失败报告里找一个失败点用工具的诊断功能打印它的逻辑锥匹配情况看在哪一级匹配断开。断开的那一级往往就是常值分歧发生的位置。然后针对这个信号分别查参考侧和实现侧的常值来源是约束给的、是优化推出来的、还是结构替换导致的查清楚来源修法自然就有了。3.4 第四步区分真常值错误与工具建模差异这里要特别提醒不是所有常值失配都是设计错误。有一部分是工具建模差异导致的比如不同工具对某个单元常值传播的激进程度不同或者对某个边界条件的处理方式不同。这类失配如果确认功能上等价可以通过工具的容差设置或者手动豁免来处理。但豁免要谨慎每一条豁免都要有充分理由并且记录下来。我见过太多项目为了赶进度大量豁免常值失配结果真问题被一起豁免掉流片后才发现。判断标准很简单如果这个常值失配能用一句话说清楚“为什么功能上等价”那可以豁免说不清楚就老老实实查到底。4. 典型场景的修复手法与参数配置4.1 综合常值传播失配的修复针对综合优化导致的常值失配修复的核心是约束同步。具体操作分三步第一从综合脚本里提取所有 case analysis 和 tie 设置第二把这些设置原样写进形式验证的约束文件第三重新跑验证确认失败点是否收敛。如果约束同步后仍有失配说明综合做了约束之外的常值推导。这时候需要看综合的优化报告找到被推导成常值的信号确认推导依据是否合理。合理的推导在验证侧补充对应的常值约束不合理的推导说明综合约束本身有问题要回头修综合脚本。一个实操细节有些综合工具支持导出常值传播报告把这份报告和形式验证的常值判定结果做交叉比对能快速找出哪些常值是综合推出来的、哪些是验证侧自己判的。两边对不上的地方就是需要重点核查的地方。4.2 扫描链常值失配的处理扫描链相关的常值失配处理顺序是先确认 scan_enable 在功能验证时被正确固定为 0再确认扫描替换的寄存器功能等价最后检查扫描链的测试模式约束是否被误带进了功能验证。如果确认是扫描替换导致的建模差异可以在形式验证时对扫描替换的寄存器做特殊处理比如指定它们的功能等价关系或者用工具提供的扫描感知比对模式。多数主流形式验证工具都有扫描链感知的选项开启后工具会自动处理扫描多路器的功能模式等价性减少这类假性失配。注意扫描链插入后的形式验证一定要用功能模式约束别把测试模式的约束混进来。测试模式下 scan_enable 为 1功能模式下为 0这两个模式的常值假设完全不同混用必然导致大量失配。4.3 时钟门控常值失配的修复时钟门控的常值失配修复要点是让门控使能的常值假设在两侧一致。具体做法从门控插入报告里提取每个 ICG 的使能信号及其常值假设在形式验证约束里逐一对应设置。对于 always-on 的使能固定为 1对于条件使能按实际条件约束。如果门控单元本身被工具建模成了黑盒需要确认黑盒模型的功能是否正确反映了门控行为。有些工具对 ICG 有内置模型有些需要用户提供模型不对也会导致常值失配。这类问题在失败报告里通常表现为门控时钟域下的寄存器集中失败定位起来比较直接。4.4 复位与初始化常值分歧的修复复位相关的常值分歧先查复位信号约束再查复位值。复位信号约束要确认极性、有效电平、异步还是同步两侧必须完全一致。复位值要确认优化过程中有没有被改动尤其是被常值传播改过的复位寄存器。工具一般支持指定初始状态或者复位状态如果参考侧和实现侧的初始状态假设不同要显式对齐。有些项目会在验证时用工具的初始化选项强制两侧从相同状态开始求解这能消除一部分初始化导致的常值失配但前提是确认两侧的复位行为本身等价。5. 排查效率提升与避坑经验5.1 建立常值假设的单一来源反复踩常值问题的项目根因往往是常值假设散落在各处综合脚本一份、扫描插入脚本一份、门控插入脚本一份、验证约束又一份四份之间没有同步机制。我的建议是建立一个常值假设的单一来源比如一份统一的配置文件综合、扫描、门控、验证都从这份文件生成各自的约束。这样任何一处改动其他环节自动同步从源头消除约束不一致。这份配置文件的内容包括所有模式选择信号的固定值、所有 always-on 信号的列表、所有黑盒的建模方式、所有复位信号的极性和复位值。维护成本不高但能省掉大量排查时间。5.2 失败点数量是重要信号前面提过常值失配的特征是失败点成片出现。实际排查时把失败点数量作为第一判断依据失败点数量在个位数优先看单个比较点的逻辑差异失败点数量在几十到几百优先怀疑常值失配和约束不一致失败点数量上千基本可以确定是全局性约束问题比如 scan_enable 没固定或者某个全局模式信号约束错了。这个经验判断能帮你快速缩小排查范围避免在错误的方向上浪费时间。我见过有工程师对着几百个失败点逐个看波形看了两天才发现是 scan_enable 没约束补上约束后失败点全消失。方向对了几分钟的事。5.3 常见问题速查表现象可能原因排查动作修复方式失败点成片集中在某模块该模块上游有常值失配查模块输入信号的常值状态对齐约束或修优化失败点集中在某时钟域该时钟域门控使能假设不一致查 ICG 使能约束同步门控常值假设失败点集中在带复位寄存器复位值或复位极性不一致查复位信号约束和复位值对齐复位建模扫描插入后突然大量失败scan_enable 未固定查功能模式约束固定 scan_enable 为 0综合后失败、RTL 仿真正常综合常值传播未同步比对综合 case analysis约束同步黑盒相关比较点失败黑盒建模方式不同查两侧黑盒模型统一黑盒建模5.4 豁免管理的纪律最后说豁免。常值失配里确实有一部分是工具建模差异功能上等价可以豁免。但豁免必须遵守纪律每条豁免记录原因、记录责任人、记录复核人并且定期回顾。豁免清单要能经得起追问任何一条说不清楚为什么等价的豁免都要重新打开查。我个人的习惯是豁免清单单独维护每次验证回归时把豁免清单和失败报告一起看确认没有新增的“顺手豁免”。顺手豁免是形式验证里最危险的操作今天顺手豁免的一个常值失配可能就是明天流片后的一个功能 bug。6. 个人实操体会常值问题导致的 formality 失败说到底是一个假设一致性问题。综合、扫描插入、时钟门控、形式验证每个环节都在对设计做假设假设不同步失配就来了。排查的核心不是逐个看波形而是把各环节的假设摆到台面上对齐。约束对齐做扎实了大部分常值失配会自动消失剩下的才是真正需要深挖的逻辑问题。我在实际项目里养成的习惯是每次跑形式验证之前先把综合和后端阶段的常值假设清单过一遍确认验证约束覆盖了所有假设再开始跑。这个前置动作花不了多少时间但能把假性失配挡在门外让失败报告里的每一个失败点都值得看。踩过几次“几百个失败点其实是同一个约束遗漏”的坑之后你就会明白排查常值问题的效率取决于你多早开始对齐假设而不是你多快打开波形。