写在前头搞数字IC验证的兄弟尤其是做后端集成或顶层签核的应该都见过Formality跑完match之后那一大串unread points的警告。有的项目里这玩意儿能直接让人血压拉满——几千个点没匹配上你根本不知道是综合脚本的问题、库文件的问题、UPF没传对还是Formality本身的配置有坑。我最早碰到这情况是在一颗MCU芯片的顶层验证上当时full chip跑匹配一上来就报了两千多个unread points吓得我以为后端网表给错了。后来一步步排查下来才发现问题出在几个看似不起眼的小细节上。今天就把这套从匹配失败到成功验证的完整处理思路写出来希望能帮被unread points折磨的人少走点弯路。1. 先把unread points这件事本身搞明白1.1 Formality到底在验证什么聊unread points之前得先清楚Formality这类逻辑等价性检查工具的工作机制。它跟跑仿真、做时序分析不一样核心任务只有一个证明两个设计在逻辑功能上是等价的。一个叫Reference Design通常是综合前的RTL或者综合后未经布局布线的网表另一个叫Implementation Design一般是经过布局布线、插了扫描链、做了时钟树综合之后拿回来的网表。Formality要证明的就是这两个设计在所有可能的输入组合下输出行为完全一致。这个证明过程分两大步第一步是匹配Match把两个设计里对应的寄存器、端口、关键net对应起来第二步是验证Verify对每一个被匹配上的点做形式化的逻辑比较。unread points就出现在第一步匹配过程中它表示design read阶段或match阶段里有一些点没有被Formality读取或无法参与匹配。注意unread不代表功能错误很多unread points本来就是可以被安全忽略的。但如果某个关键逻辑点变成了unread那就意味着Formality在这一块“失明”了后续的等价性验证结果在这些点上等于没做。这才是它麻烦的地方。1.2 unread points发生的两个阶段按我自己的经验Formality报告unread points主要在两个时间点出现处理方式完全不同。第一个阶段是读取设计的时候也就是read design之后报出来的unread points。这类点通常跟库文件、db文件、NLM(Netlist Library Mapping)文件有关。比如某个标准单元库的db里没有对应的功能模型或者NLM映射文件没给全Formality读网表时找不到这个cell的逻辑功能就会把它标成unread。还有种常见情况是用了Memory Compiler生成的macro如果没有给Formality对应的db或者lib那一整个memory block都会变成unread points。第二个阶段是match阶段结束之后报出来的unread points。这类点往往是reference design和implementation design在结构上对不上导致的。比如综合时做了retiming、寄存器重命名、常量传播又或者后端做了cell merging、buffer insertion如果svf文件Synopsys Verification Format没有正确传递这些变换信息Formality在匹配时就找不到对应关系这些点就会以unread points的形式暴露出来。1.3 unread points和failed points的本质区别这个我得多说两句因为见过太多人把这两者搞混。failed points是Formality匹配上了、也做了验证了发现两边逻辑确实不等价。这是真正的功能错误必须修。而unread points是Formality没有能力或者没有条件去验证的点它有可能是潜在的错误隐患也可能纯属合理差异。打个比方failed points相当于考试答卷里对错分明的错题unread points相当于空着没做的题——空着不一定错但你也不能说它是对的。如果一张试卷里空题太多那无论做对的题再多这份答案的可靠性都是存疑的。所以对unread points的正确态度是不恐慌不放过逐个确认原因能消的消掉确实消不掉的要有合理的解释和记录。2. unread points从哪来匹配失败背后的四类根源2.1 库文件读不完整或版本不一致这个我愿称之为unread points第一大来源。很多项目的标准单元库、IO库、Memory库分属不同团队维护交付时间也不一样很容易出现Formality用的db版本比综合时候用的旧一版或者NLM映射缺失的情况。一旦Formality在读网表时无法将一个cell的名字映射到对应的逻辑功能模型这个cell的输出端就会变成unread point。我处理过一个特别典型的事故后端给的网表里用了一个低功耗cell叫TIEHL_XXXX是一个把信号钳到高电平的tie cell。综合时用的库里明明有这个cell的db但Formality的search path里没有包含那个db文件结果这个tie cell被当成黑盒处理整条相关路径上的几百个点全部变成unread。后面把db路径补上重新读了一遍设计unread points立刻消掉了大半。所以遇到unread points第一步永远是检查你的库文件读全了没有。2.2 svf文件缺失或不匹配svf文件是综合工具Design Compiler记录设计变换过程的文件有点像一个“变更日志”。Formality读入svf后就能在reference design和implementation design之间建立对应关系比如哪些寄存器被retime了、哪些逻辑被优化掉了、哪些net被重命名了。如果svf文件没给对版本或者综合时根本没写出svf那Formality就只能靠网表结构和名字硬猜很多对不上的点自然就成了unread。这种问题在ECO流程里尤其常见。ECO之后网表变了svf没跟着更新或者ECO工具生成的patch没有同步给验证环境Formality在match时看到一堆莫名其妙的改动就到处报unread points。后来我养成了一个习惯每次跑Formality之前先确认svf文件的生成时间和网表的修改时间是不是同一个ECO版本这能省掉大量无意义的debug时间。2.3 设计层次、命名规则与uniquify问题层次化设计在Formality里有个常见痛点reference design和implementation design的层次结构不一致。比如RTL顶层下挂三个相同的sub_block综合时如果不做uniquify三个实例的原型名字都一样后端布局布线时再一改动Formality匹配时就会出问题产生额外的一批unread points。另外就是命名规则的差异。前端RTL里信号叫data_out[7:0]综合工具为了满足后端DRC或者为了解决拥塞可能把某些net改成了data_out_1、data_out_2之类的名字或者加了一堆_BUF、_CLKBUF后缀。虽然svf会记录这些改动但Formality匹配并不完全依赖名字它还有基于连接关系的匹配算法。可如果连接关系也因为某些优化变得面目全非这些点就会被漏掉。2.4 约束文件、UPF未正确传递低功耗设计越来越普遍UPFUnified Power Format文件在Formality里的地位也越来越高。UPF里定义了电源域划分、level shifter、isolation cell、retention cell等信息。如果Formality运行时没有正确load UPF或者UPF跟网表里的实际电源连接不一致Formality就可能在处理某些power-aware cell时判定为无法理解直接标unread。还有一类经常被忽略的是时钟约束和时序约束SDC。Formality虽然不做时序分析但某些约束会影响匹配。比如false path约束如果传错某些跨时钟域路径上的寄存器可能就不再参与匹配。我记得有一次就是因为一个跨时钟域的同步器被错误地设成了false pathFormality把它当成逻辑不相关的点处理结果几十个同步器全部变unread。3. 手把手处理流程从定位unread到完成验证3.1 环境准备先让工具“吃饱”处理unread points之前先确保Formality的读入环境是完整且正确的。这一步看起来基础但真的能解决一半以上的问题。我推荐在交互式命令行里跑以下操作来确认环境# 设置库路径 set search_path [list ./libs ./db ./nlm ./rtl ./netlist] set target_library typical.db set link_library * typical.db slow.db fast.db # 读入参考设计RTL或综合后网表 read_verilog -r ef_fpga_top.v current_design ef_fpga_top # 读入实现设计后端网表 read_verilog -i ef_fpga_top_impl.v current_design ef_fpga_top # 链接设计确认没有unresolved reference link读完之后要盯一下link的结果。如果有unresolved reference提示说明某些cell在库文件里找不到对应模型这往往是unread points的直接前兆。好的做法是每次读库都用sh date先打个时间戳方便记录当前用的库文件版本万一出了问题可以回溯。读入UPF也要立刻确认load_upf top.upf如果UPF文件里有错误或者警告尽早处理完再进入match阶段。UPF的报错如果被忽略后面出unread points你根本不知道是哪一步引入的。3.2 用report命令定位unread points的分布环境准备好之后读入两个设计跑到match结束就可以开始定位unread points了。Formality提供了几个非常实用的report命令# 查看design read阶段的unread points report_unread_points -type design_read unread_design_read.rpt # 查看match阶段的unread points report_unread_points -type match unread_match.rpt # 查看整体匹配情况 report_matched_points matched.rpt # 查看验证结果这里会产生verification summary verify拿到unread report之后不要直接去看那些点的名字而是先做统计分析。我自己习惯用脚本把report里的point按所在module分组看看是集中在几个模块还是散落在整个设计里。集中出现在某一两个模块大概率是库或者约束的问题散落全片可能是svf或者命名规则的问题。这样分组之后再定位效率能高不少。我记得之前遇到过一次unread points全部集中在DDR PHY相关的模块里而其他模块一个unread都没有。看到这个分布我当时就猜测是PHY的库文件或者抽象模型没给好。果不其然查了一下PHY用的lib文件是上个版本的后来升级了PHY的db重新读网表unread points直接清零。3.3 核心排查手段read_svf与set_constant的组合拳如果design read阶段已经干净了但match阶段还是报一大批unread points那基本可以确认是变换信息传递的问题。这时的核心操作是确认svf文件是否被正确读入read_svf top.svf读完之后注意看Formality的log里面会显示svf文件里的指令被执行了多少条。如果svf里的指令数和综合时报告的对不上说明svf文件可能被中间某个步骤截断过或者ECO之后没有重新生成。有时候即使svf读对了某些特殊点依然无法匹配上。这时候要分类处理。我常遇到的情况是综合把某些常量传播掉了比如某个寄存器永远被驱动为0综合工具直接把它优化没了或者变成了tie cell。这种情况下Formality需要在verify之前告诉它这个点在实现设计里已经被const掉了。做法是set_constant -type const i_riscv_top/U_ALU/r_wb_data[0] 0这个命令的意思是告诉Formality在实现设计的这个pin上逻辑值恒定为0。做完这些操作之后再重新跑match和verify这些点就不再被当成unread了。需要说明的是set_constant不是随口乱设的你必须从前仿真或者波形里确认过该信号在真实场景下确实是常量才能用这个命令。还有一个非常常见的技巧是set_user_match。有时候两边设计里明明有等价的点但Formality因为名字结构差异太大没匹配上。你可以手动把它俩对应起来set_user_match r:/TOP/U_A/reg_0 i:/TOP/U_A/reg_0_buf这个命令适合那种你清楚两边点是一回事的情况千万别拿它瞎凑匹配。不然验证结果虽然是pass的但实际验证的深度和可靠性都被打了折扣。3.4 match失败点如何逐个确认与修复对于report里零散分布的unread points逐个手动修是低效的。我更倾向于用report_failing_points把验证失败的点和unread points放在一起对比看。如果某个关键点既是failing point又是unread point那就不能靠set_constant糊弄过去了必须回到源码和网表去排查是不是综合脚本把逻辑优化错了。具体步骤是用Formality的GUI打开match窗口点中那个unread point左边是reference design的原理图窗口右边是implementation design的原理图窗口手动对比两个点的驱动逻辑。如果是简单的buffer insertion或inverter insertionsvf里应该有记录理论上不会unread。如果svf没记录那就是DC综合时某些优化选项被关掉了或者svf生成不完整。我之前抢救过一颗芯片的验证问题就出在综合时用了-no_design_rule优化选项导致DC在优化时没有把某些design rule fix的记录写进svf里。后端拿到网表后又做了DRC fix网表结构跟reference design差得有点远Formality一脸懵报了几百个unread。后面把综合脚本里那行选项去掉重新跑综合生成新svf再回来跑Formalityunread points直接降到了个位数。3.5 最终验证clean verify与报告存档所有unread points处理完毕后重新跑match加verify直到看到那句让强迫症极度舒适的“Verification SUCCEEDED”。但成功通过不算完还有几件事值得做把report_unread_points重新跑一遍确认剩下的unread points要么是设计里确实不存在的常量点要么是已经记录在案的合理差异。生成完整的match report和verification report归档到项目的验证记录里。如果有使用set_constant、set_user_match这些命令的list建议单独存档并在验证报告里注明原因。我通常会在项目的signoff目录里放一个fm/文件夹里面包含run脚本、log、report三件套。run脚本保证可复现log里面能看到当时的版本信息和环境信息report则记录下来最终验证结果的细节。下次换版本或者做ECO可以直接对比这些历史记录快速判断unread points是新引入的还是本来就存在的。4. 常见问题与排查技巧实录4.1 常见场景速查表为了让大家排查起来方便我把平时遇到的高频场景整理成一个速查表基本上unread points疑似问题都能在这张表里找到对应方向现象可能原因首选检查项常用解法design read阶段大范围unread库文件缺失、db版本不对、NLM不匹配检查link结果和db路径补齐db、更换NLM文件match阶段某个module集中报unread该module对应的库或模型未加载查看unread point所在module加载对应db或lib必要时用set_user_matchunread points伴随warning“cannot be matched”svf缺失、svf版本不对、ECO未同步确认svf生成时间与网表版本重新生成svf或补ECO patch低功耗cell导致的unreadUPF未加载、isolation/level shifter未正确处理检查UPF是否成功loadload_upf检查UPF里的供电连接tie cell大量变unread未读入tie cell所在库检查search_path补路径或用set_constant处理常量点跨时钟域同步器组变unreadSDC false path设置不当、CFS文件缺失检查SDC里CDC约束调整约束或预先set_false_path到Formality脚本uniquify不足导致多实例点匹配不上综合未做uniquify或做了又没保留检查综合脚本里uniquify选项重新综合或手动set_user_match一一对应4.2 案例复盘一次被unread points逼疯的ECO验证经历说个具体的例子那次我记得很清楚是我做一款无线通信芯片的ECO验证。后端因为芯片面积超了做了一轮functional ECO把某些逻辑从A模块挪到了B模块还把部分寄存器rename了。结果拿回来的网表跑Formalitymatch阶段一上来就爆了一千多个unread points大部分集中在被ECO改动的区域。那时候我的第一反应是svf没更新。但是查了一下ECO的patch确实也打进综合脚本了重新生成的svf文件跟网表时间戳是对得上的。这就奇怪了。后面把unread points按模块分组之后发现有两个模块明明不是ECO的重点区域却也有几十个点报unread。最后一步步排查发现是综合工具在做ECO时自动插入的spare cell被后端重新利用了这些spare cell在reference design里对应的是空的逻辑或者常量连接。而新网表里这些spare cell被接入了真实逻辑。对于Formality来说reference design里的这些点没有任何对应的参考值自然就成了unread。这个问题的解决办法是在Formality脚本里增加对这些spare cell的set_constant设置同时把这些case的例外情况写进正式的报告里经过设计团队确认后一起归档。最终验证是过了但整个过程也提醒了我一件事——ECO验证时unread points的分布往往能暴露设计改动区域处理时不能只盯着报了warning的数量更要关注哪些原本不该被改变逻辑的区域莫名出现了unread。4.3 处理unread points的三个关键动作总结这几年下来处理unread points的经验我觉得有三个动作是最关键的缺一个都可能让你在错误的路上越走越远。第一个动作是确认环境完整尤其是库文件和svf。这个动作看起来基础但它能过滤掉80%的噪声。千万别在环境不完整的情况下开始逐个分析unread point那样只会浪费大量时间。第二个动作是备份原始报告。每做一次操作比如加了db、读了svf、设置了set_constant都把当时的unread report保存一份。这样你可以随时回溯看哪些操作真正起了作用。很多时候我处理完一批unread points之后会对比不同版本report之间的差异从中能找到最重要的线索。第三个动作是留下痕迹包括svf文件、set_constant命令列表、UPF版本、库文件版本全部记录在验证脚本里有注释的地方或者单独写一个README。项目跑久了你会感谢当时那个事无巨细记录一切的自己。5. 让unread points从源头变少的工程实践坦白说unread points做到最后你会发现真正高级的玩法不是“事后处理”而是“事前预防”。在综合阶段就把验证端的需求考虑进去能让Formality阶段省下80%的力气。5.1 综合阶段就要想到Formality那头我在跑综合脚本的时候有一些固定动作是专门给Formality服务的。比如综合时一定会打开svf输出并且明确用的是write_svf确保综合过程中的每一条优化记录都被完整写出来。同时在综合完成后习惯单独跑一遍write_verilog -no_cell输出一个不带单元映射的描述这个文件在某些match阶段出错时可以用来辅助debug。另外一点综合时如果设计里有gated clock、integrated clock cell或者DFT相关的IO这些都要确保dc里的compile_ultra能正确处理并记录到svf。DFT单元的约束如果没写全后端网表里这些地方很容易产生unread。我往往会在综合时额外检查一遍所有DFT相关pin的constant设置确保DFT逻辑里面不出现Formality无法理解的悬空连接。5.2 验证环境的标准化配置Formality的脚本建议写成标准模板每次新项目直接套用。模板里面几个必选项标准单元库、IO库、Memory库、特殊cell库tie cell、delay cell、spare cell全部列清楚UPF的加载路径固定svf文件路径固定。模板里预留一个custom_overrides的位置专门放那些set_constant、set_user_match之类的例外处理命令并用注释标明每条命令的原因和日期。有了这样的模板即使是我休年假的时候其他同事也能照着模板跑一遍Formality出问题的unread points也能按模板里的注释快速理解来龙去脉。坦白说这个模板是我花了不少时间从几个项目里提炼出来的但后面它帮我节省的时间绝对远超当时的投入。5.3 从验证报告中反推设计流程的改进点还有一点我想提的是unread points的分布其实是一面很好的“镜子”它反映了设计流程中哪些环节没做好。比如你的设计里经常出现tie cell相关的unread说明综合脚本里对tie cell的处理不够规范如果memory block反复出现unread那就要看库文件交付管理是不是有问题。养成一个习惯每次处理完unread points后顺手在验证报告里写一段总结记录这些unread points的来源分类和改进建议。几个项目积累下来你会形成一份专属于自己团队的“unread points避坑手册”后面新同事接手验证工作时照着这份手册就能避开绝大部分常见的坑。我自己团队现在就有这么一份共享文档每次新项目开跑前都会翻一遍确实防住了不少重复问题。写在最后Formality的unread points这个主题说大不大说小不小。它在整个验证流程里只是一个小环节但处理不好足以卡住整个项目的signoff。我这些年处理过几百次unread points最大的体会是这问题没有银弹真正高效的解法永远是“环境干净、分类清晰、定位精准、逐一确认”。库文件读全、svf版本对齐、UPF传对、set_constant不乱设——把这几个基本功做到位unread points带来的困扰能减少八成以上。希望这篇实战指南能让大家在验证路上少踩一些坑多省一些debug的夜晚。