芯片验证这几年是越来越卷了。设计规模从几百万门一路冲到几十亿门仿真验证的人力投入常年占整个项目周期的60%以上跑一轮回归测试动不动就是几天几夜。即便这样流片前签字的那一刻大部分验证工程师心里还是没底我们真的把所有该验的都验了吗覆盖率95%意味着什么剩下那5%里会不会正好埋着一颗雷熟悉芯片行业的人都知道这种焦虑不是矫情。动态仿真的本质是抽样式测试——给出一组输入激励检查输出是否符合预期。覆盖率再高也只是测过的场景够多并不等于所有可能场景都正确。而这个行业里偏偏有相当一部分设计一旦出错就是灾难级别航空航天控制系统、汽车刹车ASIC、医疗设备核心芯片任何一个未覆盖路径都可能造成无法挽回的后果。于是验证工程师圈子里一直有一门压箱底的功夫芯片验证与数学证明也就是形式化验证Formal Verification。这篇文章我想从实际项目的角度出发好好聊聊这门功夫到底怎么入门、能解决什么问题、边界在哪里、又有哪些坑。如果你是刚接触形式化验证的验证工程师或设计工程师这篇文章也许能帮你少走很多弯路。1. 为什么芯片验证终于要搬出数学证明1.1 动态仿真的本质是抽样而非证明先把话放在前面UVM和动态仿真没有错它们是整个验证体系的中坚力量。问题在于我们经常把覆盖率达标误当成正确性达标。我做验证这些年最深的体会就是仿真验证其实是在抽样式地证明设计没有bug。你写一个约束随机测试平台生成几千几万个激励序列跑完以后看代码覆盖率、功能覆盖率、断言覆盖率。覆盖率上了90%大家觉得可以流片了。但这里面有一个数学上的硬伤覆盖率只是告诉你哪些代码被翻到了、哪些状态被溜过它没有告诉你那些还没翻到的路径里是否存在致命缺陷。举个具体例子。假设一个模块有50比特的状态寄存器它的状态空间是2的50次方大约是一千万亿的数量级。回归测试跑了一亿个周期听起来很多可折算成状态空间的百分比你连万分之一的零头都没看到。我们平时说的覆盖率达到95%往往是对代码行的覆盖不是对状态空间的覆盖。这两者的差距就是动态仿真永远无法弥合的地方。形式化验证做的事情完全不同。它不是在抽样而是在证明——用严格的数学方法在状态空间上做穷尽搜索证明每一个可达状态、每一条状态转移路径都不会触发你定义的错误属性。换句话说动态仿真是在回答我测过的情况里有没有bug形式化验证是在回答所有可能的情况下有没有bug。1.2 什么样的设计让人夜不能寐不是所有模块都让人寝食难安。数据通路上的加法器、乘法器只要功能正确仿真基本能覆盖。真正让人睡不着觉的是控制逻辑——仲裁器、状态机、缓存一致性协议、中断嵌套、乱序执行这些。为什么因为控制逻辑的问题是时序相关的bug往往藏在特定的状态序列里。比如一个轮询仲裁器正常情况下按顺序授权但当两个请求信号在某个特定时钟沿同时到达、并且队列为空、并且上一次grant刚刚释放的时候可能产生一个绕过互斥条件的窗口。这种组合场景在随机仿真里撞到的概率极低但它一旦在真实世界发生就是功能性错误。安全关键芯片就更不用说了。汽车电子里的ASICISO 26262标准对系统性失效有明确要求航空电子里的芯片DO-254把正确性证据提到了非常高的高度。这些领域里的验证工作早就不是跑得足够多的问题了你必须在文档层面给出为什么这个属性不可能被违反的论证。形式化验证的数学证明正是这种证据最直接的来源。我自己见过一个真实的案例一颗用于工业控制的设计在系统级仿真里跑了几个月所有覆盖率都达标。结果在实际现场出现了偶发性的总线死锁一个月才出现一次。后来定位到具体模块是一个内部状态机在特定输入序列下进入了非法状态。当时验证团队的第一反应是再加仿真向量去复现但几周都没有进展。最后是形式化验证工程师介入用模型检查在几分钟内给出了一个精确的反例序列。那一刻整个团队对数学证明这个词的态度彻底改变了。2. 数学证明在芯片验证里到底在证明什么2.1 先分清楚两大门类很多人一听到形式化验证就觉得是高深莫测的东西其实它在芯片验证里的落地方式主要分两类。第一类是等价性检查Equivalence Checking。它的目标很直接证明两个设计在功能上是等价的。典型场景是什么RTL修改了、ECO补丁打了、时钟门控插入了、综合后的网表要跟RTL比对。等价性检查工具会把参考设计和实现设计各自转化成某种规范形式然后用数学方法证明它们在所有输入下输出一致。这个手段在大规模数字芯片的签核流程里已经是标准动作了任何一次流片前netlist比对几乎都离不开它。第二类是模型检查Model Checking这才是很多人印象中芯片验证与数学证明的标志性部分。它的思路是给定一个系统的状态空间描述也就是RTL综合出来的有限状态机再给定一组必须满足的属性通常用SVA断言编写然后让求解器去穷尽搜索是否存在一条从初始状态出发、经过任意步转移、最终触发属性违反的路径如果不存在工具就给出proven如果存在工具会给出这条反例路径的波形告诉你具体在哪个周期、哪组信号组合下出问题。从数学角度来说模型检查是在证明一个逻辑命题M ⊨ φ。其中M是设计的数学模型φ是属性。工具输出proven就相当于在说在模型M的所有执行路径上属性φ恒真。这就是真正的数学证明而不是实验中的某种高置信观测。2.2 三个绕不开的基础断言、状态空间、求解器要理解形式化验证怎么工作必须搞清楚三块基石。第一块是断言也就是属性。形式化验证没法凭空猜你希望设计正确吗它需要你把需求写成精确的数学语句。SystemVerilog断言SVA是当前最主流的载体。举一个最简单例子假设仲裁器的grant信号不能连续两拍拉高写成断言就是grant | !grant。这句话的含义非常精确如果当前周期grant为高那么下一个周期grant必须为低。你在仿真里也会用断言但形式化验证里断言不是用来被动监控的它是交给数学引擎去证明的待证定理。第二块是状态空间。RTL中所有触发器flip-flop的取值组合构成了一个有限的状态集合。时钟沿到来时组合逻辑根据当前状态和输入信号计算出下一状态这样就形成了一张有向图——状态转移图。模型检查引擎本质上就是在这张图上做搜索。状态数量随触发器个数指数增长这也是形式化验证最核心的难点所在后面我会专门讲。第三块是SAT/SMT求解器。现代模型检查工具内部会把是否存在反例这个问题编码成布尔可满足性问题交给SAT或SMT求解器去解。简单理解SAT求解器要回答是否存在一组变量赋值使整个逻辑公式为真。如果存在那就对应了一条反例路径如果不存在就说明属性在所有可达路径上都成立。这个领域有非常深的理论积累从早期的二元决策图BDD到如今基于冲突学习的SAT算法每一步突破都在扩大形式化验证能处理的设计规模。有人问我形式化验证和普通仿真的区别我经常用一个迷宫来类比。假设整个芯片状态空间是一座巨大的迷宫错误状态藏在某条隐秘的小径尽头。动态仿真是拿手电筒去照几条路照到的路没发现问题就说目前看起来没事。形式化验证是直接调用一个数学上完备的算法把整座迷宫的所有通道都展开检查一遍然后告诉你我检查过所有路径了没有一条通往错误状态的通道。注意这不是测了很多条路而是所有路都被证明了。这个差别正是数学证明带来的独一无二的价值。3. 实操一个仲裁器形式化验证的完整流程3.1 什么样的模块适合做形式化验证先别急着学命令和脚本第一步是选对目标。形式化验证不是万能药它最擅长的是控制逻辑密集、状态空间可管理、属性清晰的模块。反过来大规模数据通路、复杂运算单元、超宽位宽的逻辑往往不适合直接用模型检查去穷尽验证。以我自己的经验这几类目标是最适合formal落地的仲裁器round-robin、priority-based、weighted等FIFO和队列的控制逻辑Cache的一致性状态机总线协议的桥接和转换逻辑电源管理状态机、中断控制器、复位逻辑。这些设计的共同特点是状态寄存器的数量通常从几十个到几百个状态空间虽然很大但对求解器来说可挑战但不至于无解同时它们都有非常清晰的正确性属性比如互斥、无死锁、有限时延响应、不丢数据。反过来如果一个模块的主要工作量在32位乘法器、浮点运算单元、或者大型加密算法引擎那形式化验证的性价比就很低——这些功能更适合用定向仿真、覆盖率统计和加速器去跑大批量数据。选型之后还有一个重要判断你要做的是证明属性成立还是寻找反例。在项目实践中很多形式化验证项目一开始的目标其实是快速找到设计里的深层次bug证明只是第二步。这个心态差异会影响你的约束宽松程度和调试策略。如果目标是抓bug你可以把环境搭得宽松一些多跑探测性质的检查让工具自由探索如果目标是签核证据那就要严格定义环境约束、覆盖率范围和证明深度。3.2 搭建验证环境的四个步骤我以一个多端口轮询仲裁器为例走一遍完整流程。假设模块有4个发起方req0到req3仲裁器按照固定轮转顺序授予gnt0到gnt3grant脉冲只持续一拍。第一步通读设计规范梳理出所有必须永远成立的性质。这一步最考验验证工程师对设计意图的理解。我会在白板上画时间序列图把关键场景标出来然后转化成断言列表。对仲裁器来说典型属性包括互斥性同一时刻最多只有一个grant有效、请求响应性如果某个req持续拉高那么对应grant必须在有限拍内到来、轮转顺序正确性grant不能跳过合法顺序等。第二步用SVA把属性写成可交工具的断言。这里有个重要经验断言要写设计必须在所有情况下满足的行为而不是某些特定场景下的预期时序。举个简化例子property p_grant_one_cycle; (posedge clk) disable iff (!rst_n) (gnt[0] || gnt[1] || gnt[2] || gnt[3]) | !(gnt[0] || gnt[1] || gnt[2] || gnt[3]); endproperty assert_grant_one_cycle: assert property(p_grant_one_cycle);这条断言说的就是如果任意一个grant信号在当前拍为高下一拍所有grant必须都为低。再写互斥断言property p_grant_exclusive; (posedge clk) disable iff (!rst_n) $onehot0({gnt[0], gnt[1], gnt[2], gnt[3]}); endproperty assert_grant_exclusive: assert property(p_grant_exclusive);$onehot0表示向量中最多只有1比特为1。这两条断言是任何仲裁器都必须保证的底线。再写一条响应性属性。如果某个请求持续有效工具需要一个公平性的描述方式。这里常见做法是用req和s_ack配合或者用带计数上限的递推形式。实际项目中形式化验证的响应性属性往往比仿真断言复杂得多因为它必须表达在任意足够长的等待后grant最终会到来而这需要借助属性中的until或eventually语义。SVA里做这类表达通常配合辅助逻辑或约束来实现这也是formal环境比UVM环境更强调验证架构能力的原因之一。第三步定义环境约束和输入假设。这一步直接决定验证的成败。外部输入如果不加约束求解器会把输入当作完全自由的变量去搜索所有可能的输入序列——包括现实中根本不会出现的输入组合。比如如果请求端口之间存在某种协议握手关系你需要用assume语句把这种关系告诉工具缩小搜索空间让它聚焦在合法场景里。还要声明时钟和复位时钟是形式化验证的时间基准复位则定义了初始状态。这些配置在商用工具里通常在环境文件里统一管理。第四步运行模型检查区分prove和find counterexample。工具一般会让你选择证明还是探测。初次运行我会先跑一个时间预算较短的BMC有界模型检查bounded model checking先快速把较浅路径上的问题暴露出来等到设计稳定后再跑无界证明尝试给关键属性一个完整的数学结论。有界的意思是检查所有长度不超过K步的路径中是否存在反例无界则是从数学上覆盖任意长度路径。两者区别直接对应实验性检查和真正证明。3.3 看到反例之后怎么读波形形式化验证和仿真的一个巨大差别在于反例通常来得又快又狠。你刚跑了一个断言工具立刻弹出一个波形告诉你第7拍grant已经拉高下一拍你期望它释放但它没有释放。这个时候你的第一反应不应该是工具是不是坏了而应该是这个反例是不是真的。我踩过的坑里第一个高发区就是反例是真实的bug还是假反例。假反例的根源通常是断言本身写得不精确、约束缺少、或者初始状态设置不对。比如p_grant_one_cycle这条属性如果设计里存在时钟门控或低功耗模式在某些拍上没有时钟沿属性用默认的采样语义就可能把两拍门控当成连续两拍grant造出假反例。这种情况要做的是修改断言的时钟事件或关闭门控检查而不是去改RTL。如果反例确实是真bug那接下来就是侦探工作。形式化工具给出的波形往往只包含与反例直接相关的信号你需要把这些信号连同内部状态变量全部拉出来看。我自己的习惯是先看反例路径从哪个周期开始出现异常倒推前面几个周期的状态转移再找到导致异常的那一步输入然后用同一组输入序列放进动态仿真里复现确认这不是工具建模偏差。这一步在工程实践里叫反例复核是所有formal sign-off流程里必不可少的一环。一个实用的调试技巧把反例拆成时间片段用二分法定位最早出现状态与预期不符的周期。比如反例一共20拍先看第10拍的内部状态是否符合直觉如果第10拍已经出问题就往前看第5拍如果第5拍还正常就检查第5到第10拍之间的输入。这样能快速收缩问题区间比盯着完整波形从头啃到尾高效得多。4. 数学证明的边界为什么不是所有电路都能穷尽4.1 状态空间爆炸是最大的敌人前面提到模型检查是在整张状态转移图上做穷尽搜索。但穷尽这个词在工程上是有代价的。一个模块如果有N个触发器状态空间就是2的N次方。N超过50时这个数字已经远超宇宙中某些物理量的数量级。即便SAT求解器有各种聪明的剪枝策略纯粹的暴力搜索仍然可能在几分钟内从正在运行变成内存耗尽。这就是形式化验证著名的状态空间爆炸问题。它决定了你能证明的电路规模存在上限并且这个上限取决于属性的复杂度和设计的相关性。同一个模块有的属性几分钟能证明有的属性跑一整夜都收敛不了。收敛不了不是工具差而是问题本身的复杂性已经超出了当前算法的可行域。应对状态爆炸工程上有几条有效策略。第一是抽象把与当前属性无关的电路逻辑从证明范围内剔除只保留与属性相关的状态变量。第二是分解把一个大模块拆成几个小模块逐个证明局部属性再通过组合论证把它们拼成整体结论。第三是假设-保证推理Assume-Guarantee把系统分成A和B两个组件先假设A的行为满足某些约束证明B在这些约束下正确再反过来证明A确实满足这些约束。这种方法在复杂互联的SoC验证中非常有用但需要你非常精确地定义组件之间的接口契约。4.2 在工程上做取舍而不是硬钢个人经验是形式化验证在项目里的定位应该是关键属性的穷尽证明而不是整个芯片的替代仿真。每次项目启动时我会和验证负责人一起做一次formal适用性评估把设计里所有模块分成三类必须formal证明的关键控制逻辑、安全相关属性、formal优先但允许部分放弃的状态空间太大但对性能有要求的逻辑、只用动态仿真就足够的大规模数据通路、运算单元。这种分级策略直接决定了人力和工具资源的分配。不要试图让formal工程师去证明一颗完整SoC的正确性——那既不可能也没必要。但反过来如果你有一个安全关键的控制模块却不安排formal证明只在UVM里跑了几万条用例就签核那就是把风险留给了硅片。还有一个经常被忽略的点formal和仿真不是二选一。很多验证团队的做法是formal早介入、仿真兜底验证。在RTL早期阶段formal往往能比仿真更早地教设计团队认清规格等设计稳定后仿真用来覆盖系统级集成的场景formal用来保证关键属性的数学正确性。两者配合效果远好于互相替代。5. 常见坑与调试技巧实录5.1 约束写得太紧量出完美但没用的证明这是我在Formal项目里见过最多的问题之一。有的验证工程师为了让求解器快速收敛给环境加了很多看起来合理的约束比如限制输入请求的间隔不小于某个周期。结果呢断言确实全部proven了但证明的只是在约束限制下的系统正确而约束本身可能漏掉了真实环境里最关键的输入场景。换句话说你证明了带套子的系统的正确性却不是裸系统的正确性。怎么避免我的习惯是给每条约束都写一段注释说明它对应的真实协议条款。签核时每一类约束都要能追溯到spec原文。如果一条约束无法从spec里找到根据那它就不应该出现在formal环境里。另外一个技巧做一轮sanity check临时去掉某些约束看工具会不会立刻抛出原本被压住的反例——如果会说明约束在掩盖问题需要重新审视约束的合理性。5.2 外部输入完全不约束搜索空间无限膨胀另一种极端是完全不约束。这会表现为formal工具长时间运行不出结果。原因很简单求解器面对的搜索空间包含了无数物理上不可能的输入序列。比如总线协议中地址通道和数据通道的握手本来有固定的时序关系但如果你没写约束形式化验证会把所有信号组合都当成可能于是它就去验证那些现实中永远不存在的激励下系统是否也正确——这么做通常只会让证明变得极其困难。解决方法是给所有外部接口建立清晰的输入假设。SVA里用assume property声明这些假设。在我做过的总线桥项目中环境约束的代码量往往是断言代码量的两三倍。这个比例听着夸张但非常真实。约束写得越精确证明的速度和可证明的深度就越高。约束本身就是验证计划的一部分应该像断言一样被评审、被review、被维护。5.3 证明不收敛时的四个排障动作当你把一个属性提交给工具跑了一整夜也没有proven也没有给反例这就是不收敛。这时候不要盲目加内存、加核数先做这四个动作。第一裁剪逻辑。把与属性证明无关的下游逻辑、调试逻辑等从证明空间里摘出去。工具通常有证明范围配置可以设置目标信号、锥形逻辑和友好边界。把问题限定到最小锥形范围内很多时候复杂度直接下降一个量级。第二增加辅助属性。某些复杂属性单独证明很困难但如果你先证明一组中间属性把结论作为假设传给后续证明整体反而会收敛。这就像做题时先证明一个引理再证明主定理。第三把无界证明降级为有界证明。如果你只是想把反例抓出来或者当前阶段不需要完整的数学结论让工具跑一个有界深度比如K50的BMC可能就够用了。它能告诉你前50拍路径内没问题虽然不等同于完整证明但在工程节奏里是一个有价值的阶段性结论。第四检查属性本身的表达能力。有些属性表述方式会引入不必要的复杂性。比如用finally、until这类时序操作符写出的属性往往比用计数器辅助实现的等价属性更难解。形式化验证的语言设计有时候需要为求解器考虑,这个经验你在写复杂SVA时一定会体会得到。5.4 反例调试的实战心得反例波形虽然只有十几拍但信息量极大。我调试反例有一套自己固定下来的流程分享给你参考。先看这个反例是属性违反还是约束违反。很多工具在找不到属性反例时会报告约束被违反——意思是说要触发这条属性失败必须同时破坏环境约束。这种情况往往说明约束和属性之间存在冲突需要回到spec层面理顺设计意图而不是直接当bug处理。再看波形中第一个不满足条件的时钟沿把它之前一个周期的各输入、各内部状态全部列出来。然后把时序往前推这条反例路径里从初始状态到第一次异常之间有几个关键状态变化把每个关键节点上哪个信号、由谁驱动、何时改变写出来。这个过程中你往往会发现是某个内部状态的判定条件漏考虑了一种组合而不是某个复杂逻辑整体出错。最后把反例中的输入序列喂给动态仿真平台构造一条定向测试用例如实测能复现那就是板上钉钉的bug。如果仿真平台无法复现你就要警惕formal环境中的抽象模型与实际电路行为不一致——通常这时我第一反应是检查时钟和复位建模第二反应是检查异步处理是否在formal环境里被过度理想化了。6. 芯片验证与数学证明我的一些实在话做了这么多年验证我越来越觉得form verification和数学证明不是一句口号而是一种踏踏实实改变做事方式的工具。它对验证团队的要求不止是会用工具更是能用精确的语言描述正确性。举个例子以前在UVM项目里验证工程师写断言经常是顺手写一条——反正仿真会跑断言失败了就报个错再debug。但在formal项目里断言就是待证明的定理你必须反复推敲它的每个时序细节。这种严谨性训练对验证工程师的成长帮助巨大。我带过的团队成员凡是认认真真做过一两个formal模块的回去再写仿真断言的质量都明显上了一个台阶。再说说角色定位。有些人觉得formal验证的存在会取代传统UVM验证工程师我的看法完全相反。formal解决的是关键属性的穷尽证明仿真解决的是系统集成和交互的广泛覆盖。一颗复杂的SoC如果没有UVM去做端到端的大场景验证光靠formal在模块级证明根本无法发现总线互联、中断路由这些跨模块交互问题。反过来也一样如果把formal工程师只当作仿真团队的辅助让他们在回归测试里帮你跑跑断言那就是大材小用。最好的状态是两类工程师在项目里以一种互补的方式合作formal早介入仿真兜全流程两者共享同一套断言库和覆盖率分析方法。最后说一句关于安全标准的事。这几年ISO 26262、DO-254这些安全标准在验证方法学上的要求越来越明确形式化方法已经成为许多安全关键项目中正确性证据的重要组成部分。如果你正在做汽车、医疗、工业控制相关的芯片form verification已经不再是一个可选项而是迟早要被摆上台面的硬需求。哪怕你现在所在的项目还没有强制要求提前把形式化验证的方法论学起来、在非关键模块上练起来都是非常值得的投入。我自己的体会是用数学证明的方式看RTL会改变你对验证完成的定义。以前我说验证得差不多了心里其实知道这不是证明现在我会区分仿真测过了和数学上证明了。这之间的差别可能就是一次流片事故和一次顺利量产之间的距离。希望这篇文章能帮更多验证工程师把这条数学证明的路走通。