形式验证学习笔记：从仿真盲区到穷尽式验证

入这行头几年我一度觉得形式验证是个偏“玄学”的东西。求解器、状态空间、二元决策图听上去全是数学和底层实现跟每天跑回归、调UVM环境的验证工程师隔着一层纱。直到有次回片后一个只在超长指令序列下才触发的死锁问题用动态仿真怎么都复现不出来了我们才把形式验证当成最后救兵。从那时起我认真把这套方法捡起来系统啃了一遍边学边在公司真实项目里试踩了不少坑也补齐了过去验证思维里的一个大盲区。这篇文章就是我整理出来的学习笔记。不讲虚的里面既有形式验证的整套认知框架也有我实际跑通的工具流程和操作细节还包括经常遇到的坑。不管是刚开始接触形式验证的芯片验证工程师还是想评估“形式化方法到底值不值得引入”的项目负责人这份笔记都能提供一些可落地的参考。顺便说一句形式验证不是来替代动态仿真的它解决的是动态仿真最头疼的那类问题——路径太长、组合爆炸、靠采样根本覆盖不到的场景。1. 先建立直觉形式验证到底在做什么1.1 一次动态仿真查不出来的bug我以前一直认为验证嘛无非就是搭testbench、撒激励、比对结果。回归跑得越多覆盖率越高芯片就越稳。直到那个死锁问题出现才让我意识到仿真本质上是在“采样”是对海量状态空间中的一小部分路径做抽样检查。那个死锁bug就藏在两个模块的状态机交互里。单条路径怎么跑都正常必须让A模块处于某个特定内部状态同时B模块在特定时刻发出请求再加一个跨时钟域的偶然时序错位几百万条随机仿真里都不会碰上一次。这类bug属于“长尾事件”仿真覆盖率再高也总有一片区域永远触达不到。形式验证正是解决这类问题的它不是随机撒激励而是把整个设计建模成数学对象用算法去证明“在所有可达状态下某条属性是否永远成立”。这里的关键词是“所有”不是“很多”也不是“足够多”。它是穷尽式的、数学层面的完备性判定。这对我的冲击很大——原来验证还可以回答“永远不会发生什么”这种问题。1.2 动态仿真与形式验证的本质差异动态仿真说白了就是“举例”你写一千条用例设计就回答一千次这千次都通过不能说明万无一失。形式验证则是“证明”它把设计的状态空间、输入约束、期望属性全部形式化再让求解器去遍历或推理。用一句通俗的话来比喻动态仿真像猎人在大片森林里打猎能不能打到猎物取决于运气和路线形式验证像给整个森林修围墙只要墙修得够高你从数学上知道猎物出不去。代价是修围墙往往比打猎复杂得多——状态空间一大求解器也会“跑不动”。所以成熟的团队不会让形式验证包打天下而是把它用在“仿真覆盖得很吃力的关键控制逻辑”上。这也解释了为什么形式验证在工业界一直给人“门槛高”的印象。它不是那种写下testbench就能自动跑的东西它需要使用者理解设计、会建模、能写属性还要懂得怎么控制复杂度。但一旦用对了地方回报非常直接有些bug仿真跑几个星期都发现不了形式验证一夜之间就能给出反例。1.3 两大技术分支等价性检查和模型检查形式验证在数字芯片领域通常可以分成两个主要方向最好一开始就把它们分清因为它们的应用场景和工具链完全不同。等价性检查Equivalence Checking缩写EC的核心问题是两个设计在功能上是否等价最典型的场景是后端流程——逻辑综合后门级网表跟RTL是否一致、扫描链插入后是否破坏了功能、ECO修改后是否保持行为不变。它面向的是“前后两个模型之间的一致性”以组合逻辑等价性为主借判定图和SAT求解器来完成已经是一项相当成熟的技术几乎所有芯片流片流程都会默默用到。模型检查Model Checking则更“前端”给定一个设计模型和一组需要满足的属性验证设计是否满足这些属性。比如“两个master永远不会同时拿到总线授权”“请求发出后50拍之内一定收到响应”。它面向的是RTL本身的行为正确性是传统仿真验证在“完备性”上的直接补充。商业工具里JasperGold、Questa Formal为代表开源生态里SymbiYosys的prove模式也属于这一类。学习时我建议把这两条线分开走因为EC相对更“机械”、更容易自动化而Model Checking更考验使用者对设计逻辑和属性的理解。先掌握EC熟悉形式化思维再转向属性验证节奏会顺畅很多。2. 拆解底层原理求解器凭什么敢说“穷尽了所有可能”2.1 状态空间与有限状态机模型形式验证能“穷尽”所有情况的根本前提是把数字电路建模成有限状态机。不管一个寄存器设计眼前的行为多复杂它归根结底是一组布尔状态变量再加上输入信号共同决定了下一拍的状态和本拍的输出。以一个简单状态机举例假设设计里有三个寄存器那么它最多有2的3次方也就是8个可能状态每拍状态在输入驱动下发生迁移这些迁移关系可以用逻辑公式严格刻写。形式验证要做的就是在这张状态图上做数学推理从初始状态集出发哪些状态能够达到这些可达状态是否会触碰某个坏状态或者是否存在一条无限路径违背时序属性。验证问题的“完备性”也从这里来。只要你能准确描述初始状态、状态转移关系和待验证属性那么证明结果是确定的——要么属性确实对所有可达路径成立要么能给出一个具体的反例路径。这种“要么证明要么反例”的二元输出是形式验证区别于动态仿真的根本魅力。当然代价也很直观。寄存器一多状态数量就指数膨胀几个上百个寄存器的设计全状态直接超过可观测宇宙的原子数这种情况下没法真去“遍历”。形式验证的学问就是怎么在这种情况下依然完成推理这就要靠下面说的底层引擎。2.2 三类核心引擎SAT、SMT与BDD形式验证工具内部依赖的求解技术换了一代又一代但核心还是几类引擎。SAT求解器解决的是布尔可满足性问题。你给它一个由与、或、非组成的布尔公式它判断是否存在一组变量的赋值让整个公式为真。听起来是很简单的问题但现代SAT求解器通过CDCL算法冲突驱动的子句学习能在数百万变量的规模上高效工作。大部分等价性检查和有界模型检查都会把验证问题转化为SAT问题来求解。SMT求解器是SAT的扩展版允许公式里出现整数、位向量、数组等高级理论复杂度更高但表达也更自然。比如CPU里一条加法指令的结果用位向量表达会比展开成几千个布尔变量高效得多。开源生态里的Z3就是一个典型代表SymbiYosys的prove流程经常需要它。还有一类基于BDD的符号方法。二元决策图通过变量排序和节点共享能把很多布尔函数表示得异常紧凑。当年的符号模型检查主要靠它至今部分等价性检查场景里仍然在用。它的问题在于遇到某些规律性差的逻辑比如乘法器图会急剧膨胀所以工具里往往以上几种引擎混合使用。理解这些引擎不必过分深入细节但有一个思路值得记住形式验证工具并不是什么“魔法”它本质上都是把验证问题转化为某种数学问题然后交给算法去求解。理解了这一点后续做的很多操作——切分、抽象、约束——其实都是在帮求解器降低问题的难度。2.3 为什么不用“暴力穷举”抽象、归纳与反例引导既然不能真穷举全部状态那么工业级模型检查是怎么完成的这里有几类关键思想值得知道。有界模型检查BMC是最直观的一个思路我不证明全部长度路径而是先假设只在K拍以内检查属性存在违背就把反例找出来。它的核心价值在于“找bug”通常很快就能发现很深的bug因为SAT求解器找反例的能力确实强。代价是若没有反例也不代表属性一定成立只是说明“前K拍没发现”。为了做到“无界证明”现代求解器大量使用基于归纳的方法以及IC3/PDR这类代表性算法。IC3的思想很有意思它用一组不断精化的“归纳状态帧”去逼近所有可达状态既能证明安全属性也能找到有界反例。这些算法让模型检查有能力处理包含几万寄存器的实际设计——不是靠穷举而是靠聪明的逻辑推理和后端剪枝。此外还有抽象与精化技术。工具可以把某些无关的状态变量抽象掉先在一个更粗糙但更小的模型中证明如果发现了反例再判断反例是否真实成立不成立则通过“反例引导”细化模型循环下去。这也解释了为什么实际使用形式验证时结果经常出现UNKNOWN或者超时——工具已经在内部做大量试错能收敛就给你答案收敛不了就卡在那里。我们作为使用者能优化的就是尽量让工具的推理过程更轻松。3. 实操流程用开源工具跑通第一个等价性检查3.1 工具选型商业工具与开源工具怎么选学习形式验证工具选型第一大现实问题。商业工具中等价性检查用得最多的是Synopsys的Formality模型检查则是Cadence的JasperGold和Siemens的Questa Formal。这些工具功能细致、文档完善普遍用在正式流片项目里但个人学习很难拿到授权也不太适合在家里折腾。开源生态让我这种个体学习者有了很顺的上手路径。Yosys是一套开源RTL综合工具它支持读入Verilog并进行formal模式的编译SymbiYosys是建立在Yosys之上的形式验证流程框架可以调用多个后端求解器比如内置的smtbmc、abc以及外接的Z3等。你还可能用到NuSMV这类经典模型检查器。整体来说用Yosys加SymbiYosys加Z3这套组合学完基本概念和流程完全够了而且跑小例子速度很快。我的建议是先别纠缠工具选型问题把开源这套装好跑通理解形式验证工作流的“阅读设计-设置模式-约束环境-发起证明-分析反例”这段循环再考虑要不要接触商业工具。形式验证的理念和流程是通用的换了商业工具底层的思考方式完全一样只是命令和界面有差异。3.2 环境搭建与第一个等价性检查流程以Ubuntu环境为例安装Yosys和SymbiYosys的基本路径大致是从GitHub拉取Yosys源码编译期间会用到gcc、bison、flex、readline库等依赖编译完成后再把SymbiYosys的代码拉下来确保能运行sby命令。如果不想折腾编译也可以直接用现成的Docker镜像几条命令就能把环境拉起来少踩很多编译的坑。等价性检查我建议直接用一个简单案例来体会。比如我们有一个旧的RTL文件decoder.v和一个经过手工“优化”的新版本decoder_opt.v想验证两者在所有输入下输出是否一致。流程大致如下# 读入两个设计 read_verilog decoder.v read_verilog decoder_opt.v # 指定顶层模块 prep -top decoder -flatten # 等价性检查相关命令 equiv_make decoder decoder_opt equiv_decoder # 进行匹配与证明 equiv_simple -seq 2 equiv_induct -seq 2 equiv_status -assert第一次跑通时我最大的感受是原来形式上证明两个设计等价并不需要撒一条激励它是在逻辑层面对两个设计中对应的门网络做匹配和推理。凡是工具能匹配上的点直接简化匹配不上的进入求解验证。这就是为什么EC能对各种复杂改动给出结论——“改过的这个大逻辑块新老版本表现完全一致”。等价性检查要想跑得顺利有几个重要前提两个设计的寄存器数量和状态定义要能对应得上如果做了重定时或者状态编码调整普通组合EC会不认账需要额外处理还有别忘了设置合理的时钟约束和边界条件。初学阶段容易踩的坑包括没加glbl文件导致未知状态处理不当、时钟信号没有正规化导致匹配错误、跨模块边界被flatten后出现多个同名寄存器等。3.3 从反例到调试第一个等价性检查失败怎么办等价性检查如果失败工具通常会给出反例信息告诉你“在这组输入下旧设计输出为0新设计输出为1”。拿到这种反例第一反应不要立刻怀疑工具九成情况是设计确实被改出了差异要么是功能改变要么是改动时某个位宽没对齐。我调试时习惯用这样的流程先看反例给出的输入向量能否应用在真实场景中有些反例只会在不可能的输入组合下出现这就说明是约束不足如果输入组合在真实场景里确实会出现那就说明新版本可能在功能上做了改动需要跟负责人确认是否故意为之还有一种情况是新旧设计都正确只是某个对于形式验证很关键的点比如比较点的使能条件设置不对导致报了伪反例。排除这种伪反例通常需要在设置里补充合理的常量约束和条件。这个调试过程让我对等价性检查有了更深的信任感。它不是空口说绝对等价而是给出一个可读、可分析的构造性反例让工程师能快速定位到具体逻辑分支这比动态仿真中的波形比对更直接。4. 属性验证实战从SVA断言到模型检查4.1 SVA断言形式验证与仿真相通的语言模型检查的核心输入是属性而业界最常用、跟动态仿真也共通的属性语言就是SystemVerilog AssertionsSVA。在学习SVA时我忽然意识到这玩意并不只属于形式验证——在UVM仿真中也可以写SVA仿真时会随激励一起检查时序。区别在于形式验证中SVA会成为证明目标而不是只在撒到激励时被触发。SVA的基本形态先说清楚。即时断言immediate assertion只是“断言这一刻条件是否成立”比如assert (a !b) else $error(...)。并发断言concurrent assertion则用于描述跨拍时序关系写法通常是assert property((posedge clk) 前置条件 |- 后续条件)|-的意思是“当前拍满足前置条件后下一拍开始检查后续条件”而|则代表“隔一拍再检查”。后面还会用##[1:5]表示1到5拍的窗口。举个最简单的互斥性断言例子。一个二选一仲裁器要保证两个输出不能同时拉高module arbiter( input clk, input rst_n, input req0, input req1, output reg gnt0, output reg gnt1 ); // 简化的轮询仲裁实现…… // 形式验证要证明的关键属性 assert property((posedge clk) disable iff (!rst_n) !(gnt0 gnt1)); endmodule对初学者来说SVA里面最有价值的认识是属性本身需要精确到你真正关心的行为。互斥性是一个“永远不该发生”的坏事属于安全属性响应性则是“请求最终会得到响应”的好事属于活性属性。后者证明起来往往比前者难得多因为需要处理“最终”的概念工具可能要展开很长的路径或者做更复杂的归纳推理。给初学的朋友一个操作建议学习SVA时先在仿真环境里跑通等发断言能在波形中正常亮红灭红再搬到形式验证工具中去试。SVA里面的$rose、$fell、$stable、##[0:$]、[*0:$]这些语法不要死记写上几个例程一跑看波形自然就记住了。4.2 用SymbiYosys跑通一个属性证明属性验证怎么在开源流程里落地我用一个带写和读的FIFO设计来说明。假设FIFO顶层模块叫fifo.v内部寄存器实现了读写指针和空满标志。我要证明的核心属性是当full信号为高时写请求不会执行。写成SVA后增加到RTL里然后创建一个.sby配置文件[options] mode prove depth 100 [engines] smtbmc z3 [script] read -formal fifo.v prep -top fifo [files] fifo.v然后运行sby -f fifo.sby运行后如果属性成立控制台输出会明确提示成功如果存在违例工具会把反例波形导出用常见的波形查看器打开就能看到在哪一拍开始违反。我自己第一次跑通时惊讶于整个流程的轻量——没有testbench场景编写不需要给激励只需要设计本身、配置文件和想证明的属性后面全部是求解器在“思考”。不过要注意mode prove和mode bmc的区别。bmc只是有界检查只查有限拍内是否存在反例适合找bugprove则尝试做无界证明潜力更大但也更耗时。初学阶段可以先跑bmc看反例找得快跑通之后再切到prove验证正式属性会比较友好。4.3 属性验证容易忽略的环境建模真正在形式验证环境中证明一个属性光是把SVA写对还不够还要把环境约束写全、写精这部分最考验经验。一个常见的错误把属性里的“前置条件”当成了所有情况都要满足的真相。比如一个DMA模块你希望证明“当软件设置描述符有效时对应内存访问一定在若干拍内发生”。如果不在环境约束里说明“软件只能在后端空闲时发出请求”验证工具就会假设任何时刻都可能出现任意请求甚至出现软件同时发起两个明显互斥的操作导致证明失败。这种为工具补充的环境约束在SVA里用assume来表示。比如“写端口的写使能never同时为高”这条约束作为assume告诉求解器这个输入组合根本不会出现在真实环境中对应的“输出不会同时为高”则是assert是需要被证明的结论。还有一个关键的经验是在顶层属性验证时reset和clock的建模一定要干净。异步复位之类的情况要处理好不然工具会认为复位信号也能随便变化推出各种反例来误导你。我们做项目时通常会把复位置成一个初始状态之后保持不变再用disable iff排除复位状态的检查这样可以让证明问题更收敛。形式验证有个术语叫“vacuous pass”意思是属性通过了但是因为它只适用于一个空集等于啥也没证明。比如前置条件永远为假那整条属性就是“空过”。这种情况在团队review时非常容易漏掉。我的习惯是每声明一个assume变量都会问自己这个assume会不会太强如果有任何可能把真实合法的场景也约束掉了那证明结果再漂亮也是假的。5. 常见问题与避坑来自项目一线的经验总结5.1 到底哪些设计适合做形式验证刚学形式验证时我像个拿着锤子的人见什么都想砸一下。后来才知道能不能用形式验证首先取决于设计本身的结构特征。比较适合的形式验证对象通常有这么几个特征首先是控制逻辑为主比如仲裁器、协议状态机、中断控制器、FIFO的读写控制其次是属性比较明确比如互斥、一次握手、有限时间内的响应再次是复杂度适中寄存器数量不能过大到不可控但经验丰富的工具使用者可以处理几万寄存器的设计。不太适合的对象很快也会暴露大规模数据通路比如巨大的乘法器、复杂的DSP计算单元这类设计状态空间虽然可以建模但求解器面对位向量算术时往往力不从心随机性很强的系统级事务交互模型如果属性本身描述不清楚证明更是无从谈起还有那些大量使用黑盒IP、时序约束复杂的设计建模本身就会占据大量时间。一个比较稳妥的落地策略是“关键控制模块优先”。每个时期选一两个影响系统安全的核心模块写清楚关键属性跑形式验证把仿真里最容易漏掉的死锁、活锁、协议违例这类问题用形式化证明兜底。没必要指望整套芯片全形式化那不现实也不经济。5.2 状态空间爆炸的应对办法状态空间爆炸是形式验证最现实的敌人我相信每个用过JasperGold或SymbiYosys的人都在等待证明时体会过它的可怕。起初看着求解器跑了几个小时不结束只能干着急。后来积攒了一些应对手段。第一个思路是“切分证明”。把一个大模块拆成若干子模块分别针对子模块做假设和证明再通过assume-guarantee的推理一层层组合起来。比如想要证明总线上所有master都遵守仲裁协议可以先分别对已知master建模再组合看总线是否仍然安全。第二个思路是“做抽象”。找出证明目标不需要关心的数据和信号用更简单的模型替代或在证明中忽略。比如只关心控制状态机不关心数据总线上的具体数据就可以把数据信号抽象成一组自由变量。抽象做得好的话证明时间有时能从几小时降到几分钟。第三个思路是在属性本身上花功夫。把“大属性”拆成若干“小属性”或者给某些内部信号增加额外的中间断言让求解器能够在更小的子问题上分离推进。这跟写软件时拆函数是一个逻辑问题切小了求解器才有机会用归纳和剪枝快速收敛。实际做下来这种手工的“证明设计”往往是形式验证工程师最核心的日常工作量。5.3 学习形式验证最常踩的几个坑复盘我自己的学习过程有几个坑反复出现写出来供参考。一是“初始状态没设对”。形式验证对初始状态极其敏感如果初始状态集合跟真实上电情况不一致证明结果就没什么参考价值。这也解释了为什么很多工具都会提供一个“初始化寄存器”的环节有必要时还得自己补充约束。二是“异步逻辑模型处理不当”。形式验证本质上是在理想化的同步模型上做推理异步接口、类似握手和跨时钟信号如果不做规范化建模工具会给出各种看起来很奇怪的反例。最好把跨时钟信号当抽象输入或加约束处理不要在证明中硬碰时序细节。三是“只关注assert而忽略assume”。属性验证的环境约束很多时候比断言本身更考验功力。一个经验是每当证明超时或卡死先反过来审查一下现有assume是否合理有没有过强或过弱往往比闷头等求解器更有效。四是“结果过得太快也要警惕”。如果一条属性两三秒就证明完毕不一定是你厉害可能是属性本身非常平凡甚至是个空过。检查一下属性前置条件有没有可能被assume约束成永远为假再确认一下覆盖动机cover property有没有被工具实际触发过这种确认并不复杂但能避免提交一堆“看似证明成功实则没检查到东西”的属性。6. 学习路线再复盘我是怎么把形式验证用起来的如果让我把形式验证的学习路线再浓缩一遍大约可以浓缩成四层理解“证明思维”、看懂底层求解器、熟练属性编写、掌握抽象与收敛技巧。第一层建议先搞明白“形式验证到底能回答什么问题”。带着具体问题去学比泛泛了解效率高得多。我当时就是因为死锁问题才下决心学的学习的每一步都能对照真实场景理解也更快。第二层要看懂一点SAT和SMT求解器的工作原理。不求推导算法起码要明白求解器为什么在某些问题上能秒解、在某些问题上却卡死。这决定了后续做约束和抽象时你能不能在直觉上判断哪些操作会更有效。第三层是动手写SVA。从最基础的断言开始逐步加入时序、窗口、重复算子、disable iff等语法。每写一条属性都要结构清晰养成先写注释说明“这条属性防止什么bug”的习惯。团队协作时这一点尤为重要。第四层是真正接触项目的工程化问题。在项目中先选一个受控模块试点列出最需要保证的属性清单逐个形式验证记录超时、卡住、抽象等过程。有了这段经验你就能判断哪些模块适合形式验证、适合哪种工具、瓶颈在哪里也开始积累自己的“属性库”。四层走完之后形式上的一条条命令和语法已经不再重要重要的是你已经建立起了“这套设计的行为边界到底在哪里”的思维模式。这种思维反过来也会提升你的仿真验证水平——你会自然而然地知道哪些断言值得写哪种覆盖策略更重要甚至能提前嗅出某些设计结构的风险。我自己现在做项目时形式验证并不是孤立存在的它是我验证工具箱里的一件重要工具和动态仿真并列使用。动态仿真跑大面上的行为兼容与数据完整性形式验证维护几条关键的安全属性和协议属性两边消息互通一有设计改动就把回归和形式验证一起跑覆盖面和效率都比之前单打动态仿真时好很多。当然要把形式验证配置稳定在工程流程里前期投入不少但一旦形成了一套可复用的属性库和环境脚本后期维护成本其实很低回片后的“没想到”时刻也少了很多。最后再分享一个小技巧学习阶段别贪多从头到尾手工跑通一个FIFO或仲裁器的属性验证比看十篇理论文章都有用。你会真实地体会到什么是“状态空间爆炸”什么叫“assume写错的后果”什么叫“反例出来时眼前一亮的快感”。这些体验攒够了形式和仿真在你心里的位置自然会像在项目里一样各归其位。