JasperGold实战：乘法器形式化验证从断言到收敛

简介基于JasperGold的Booth乘法器形式化验证源码包面向数字IC验证工程师、芯片设计学习者及EDA工具使用者用于快速搭建形式化验证环境并理解核心验证流程。资源共7个文件包含2份Markdown说明文档讲解思路与步骤、1个TCL验证脚本实现自动化验证、1个C黄金参考模型模拟乘法器行为、1个Verilog设计文件被测RTL及配置文件整体仅9KB轻量精炼。目前已有126人学习下载。包内内容围绕乘法器模块验证展开涵盖输入输出信号定义、黄金模型宏定义与条件分支处理、TCL脚本自动化任务、virtual_net简化RTL逻辑以及proof_structure控制验证步骤等关键环节同时穿插分支断言处理和验证空间优化的技术细节。读者可参考完整源码与注释快速复现验证场景减少脚本调试成本提升对JasperGold形式化验证方法的实际运用能力。1. 项目背景与核心价值拆解做芯片验证做了这么多年我最常被问的一个问题是“仿真都过了还要形式化验证干什么”尤其在乘法器这类纯数学模块上很多人觉得用定向测试加随机激励撒几千个case就够了没必要上JasperGold这种重型工具。但等你真遇到一次因为乘法器进位链在一个极端组合下算错、导致RTL在硅片上跑出脏数据的事故就会明白仿真永远只能证明“测过的地方没问题”而形式化验证能证明“所有输入都没问题”。JasperGold是Cadence家的形式化验证平台行业里习惯直接叫它JasperGold命令行默认也保留了jxg这种缩写。它解决的核心问题只有一个把你的DUT火星四射地塞进一个数学空间里用SAT求解器、BDD、SMT这类引擎去穷尽所有输入组合验证你写的property在所有可达状态下都成立。你不需要造上百万条激励只需要写对一个断言剩下的交给引擎去暴力穷举。那为什么说乘法模块尤其适合用JasperGold验证因为乘法的数学规律非常明确非常容易写出一个“必须为真”的断言。比如a * b的结果必须等于你用一个参考模型算出来的结果或者满足某种恒等式。相比之下你要验证一个DMA控制器的状态机光是把状态定义清楚就得费不少功夫property跟实际意图之间还隔着一层“有没有理解对”的风险但乘法器不存在这个问题——数学就是数学公式是死的断言错了只能是你参考模型写错了。这篇东西就是围绕“怎么用JasperGold对乘法模块做验证、源码怎么组织、证明跑不动了怎么调”来讲的适合刚接触formal验证的DV工程师也适合想把手头乘法器验证做扎实的IC设计工程师参考。我尽量不写“说明书体”全部按我在真实项目里踩过的坑、验证过的方法来讲。2. 乘法器验证难在哪组合空间和时序细节你可能觉得乘法器有什么难验证的不就是输入两个数、输出一个积嘛。但实际做起来有俩坎儿一个是空间爆炸一个是时序边界。先说空间爆炸。假设乘法器输入位宽是WIDTH 16两个操作数就是32个bit再加个使能信号、模式选择信号输入状态空间轻松到几十个bit。如果是仿真2的32次方种组合你跑死也测不完。但对JasperGold来说这不是靠随机采样去碰运气而是在布尔逻辑的层面直接证明“对于所有满足约束的输入组合断言都成立”。当位宽涨到32位、64位甚至带符号、带累加的乘加单元时证明过程就会面临“状态爆炸”这就是形式化验证里最实在的难点——不是不会做是做不完。再说时序。乘法器在流水线里往往不是一拍出结果有的设计是两拍、三拍甚至带握手信号的。你写property如果不知道输出到底在哪一拍有效断言会出来一堆假反例。看波形的时候你会发现引擎报的“FAIL”根本不是逻辑错而是你时序没对齐。这个在我刚做formal那几年吃了不少亏。另一个容易被忽略的点是使能信号和复位行为。很多乘法器的RTL会在使能无效的时候保持输出不变或者复位后输出清零。你写断言如果拿一个自由跑的a*b去跟DUT的输出比引擎一秒钟就能给你找出反例使能拉低、输出寄存器保持旧值而你期望它等于当前输入算出来的积。这种反例是“真反例”但根因是断言写得不够严谨不是RTL有bug。所以在动手写property之前第一步不是写代码而是先把DUT的接口时序捋清楚输入什么时候有效输出什么时候有效有没有valid握手使能无效的时候输出是什么行为。这个搞不明白后面全是白干。你可以画一张简单的时序图贴在工位上也可以直接在源码注释里写清楚总之不能含糊。乘法器还有一个比较特殊的地方——它经常是“组合逻辑 输出寄存”的结构也就是数据通路上没有状态。这种情况下JasperGold的证明难度主要在组合逻辑规模上而不是状态空间的深度上。引擎处理起来会比带复杂状态机的模块更容易收敛但反过来一旦组合电路里的某个进位逻辑写错了在仿真里你可能要撞大运才能触发而在formal里只要断言绑对几秒钟就能把角落里的错挖出来。这也是乘法器验证最爽的地方。3. 源码结构与形式化测试平台搭建3.1 Formal Testbench的组成骨架用JasperGold验证乘法器不是把RTL拖进去就跑的你需要搭一个专门的formal testbench通常叫tb_formal或formal_top。它的构成和仿真testbench不太一样核心是两个东西约束constraint和断言assertion。约束用assume来写作用是限定输入的合法空间比如“输入只允许在0到1000之间”“使能信号与valid必须同拍拉高”。断言用assert来写这是你要证明的规则本身。JasperGold的验证流程就是在所有满足约束的输入序列下检查断言是否永远成立。一个典型的乘法器formal testbench骨架长这样module formal_multiplier_tb #( parameter int WIDTH 16 )( input logic clk, input logic rst_n, input logic en, input logic [WIDTH-1:0] a, input logic [WIDTH-1:0] b, input logic valid, output logic [2*WIDTH-1:0] product, output logic out_valid ); // 参考模型计算结果 logic [2*WIDTH-1:0] ref_product; always_comb begin ref_product a * b; end // 输入约束en/valid同时有效时a和b任意值均可 // 但en无效时不做比较用implication限定 default clocking cb (posedge clk); default input #1step output #0; endclocking property p_product_valid; (posedge clk) disable iff (!rst_n) (en valid) |- ##[1:3] (out_valid (product ref_product)); endproperty assert property (p_product_valid); endmodule这段代码里最关键的一行就是(en valid) |- ##[1:3] (out_valid (product ref_product))。意思是当en和valid同时为高时往后1到3拍内out_valid必须拉高且product必须等于当前拍输入的a*b。这个##[1:3]就是处理流水线延迟的容差窗口你需要根据DUT实际的流水级数去调不要一刀切写死成##1。另外注意ref_product是用always_comb算的这是纯组合参考模型。如果你用的工具支持也可以直接用let定义比如let ref_product a * b;效果类似但let在property里的作用域更干净遇到复杂表达式时可读性更好。3.2 Bind方式与源码组织formal testbench和DUT的连接行业惯例是用bind。好处是不用动DUT的源码验证代码独立管理而且多套验证环境可以共存。给乘法器模块multiplier_top做验证bind大概长这样bind multiplier_top formal_multiplier_tb #( .WIDTH(32) ) u_formal_tb ( .clk (clk), .rst_n (rst_n), .en (en), .a (a), .b (b), .valid (valid), .product (product), .out_valid(out_valid) );整个工程目录我习惯这么分multiplier_verif/ ├── rtl/ │ ├── multiplier_top.sv │ └── multiplier_core.sv ├── formal/ │ ├── formal_multiplier_tb.sv │ ├── formal_bind.sv │ ├── properties.sva │ └── constraints.sva ├── scripts/ │ ├── run_jasper.tcl │ └── compile.f └── logs/properties.sva只放断言属性constraints.sva只放约束这样当你需要跑不同位宽、不同模式的验证时可以快速切换组合。源码里注释一定要写清楚“这个property对应需求文档里的哪一条”不然三个月后你自己回来看都不知道当初为什么这么写。这里有个很实在的教训bind的实例名和内部信号名在JasperGold的GUI里都会体现出来。如果命名太随意比如u_tb、a、b这种排反例的时候你会在原理图里找得想骂人。正规的分层命名是u_formal_tb、core_a_i、core_b_i这种一眼能看懂在DUT的哪个层级。花十分钟取名字后面能省两小时。4. 关键Property的写法与验证策略4.1 不等价类断言把bug逼出来做乘法器验证我最推荐的断言思路是“对照参考模型做等价比较”这是最高效、最直接的策略因为它不需要你去理解RTL内部每一位的运算细节。你只需要保证参考模型是对的然后让JasperGold证明“在任何合法输入下DUT输出始终等于参考模型”。刚才测试平台里的写法就是最基本的形式。但实际项目里乘法器往往不是简单输出a*b还会有符号扩展、舍入、饱和、截位这类操作。这时候参考模型也要跟着做同样的处理否则断言必挂。比如有符号乘法logic signed [WIDTH-1:0] a_s, b_s; logic signed [2*WIDTH-1:0] ref_s; assign a_s a; assign b_s b; assign ref_s a_s * b_s; property p_signed_product; (posedge clk) disable iff (!rst_n) (en valid) |- ##[1:3] (product ref_s); endproperty这个看着简单但特别容易踩坑的是SystemVerilog里把一个logic [WIDTH-1:0]和另一个同宽度的信号相乘在赋值给2*WIDTH位宽的结果时无符号数和有符号数的位扩展行为完全不一样。如果你DUT内部用的是补码乘法器而参考模型忘记加signed声明JasperGold十秒钟之内就能给你抛出一堆反例而且指向完全正确的数学错误。这种bug在仿真里要是不刻意覆盖负数和正数边界很容易漏掉但在formal里简直就是送人头。除了对照参考模型我还会写“代数恒等式”性质来交叉验证DUT行为。比如乘法的交换律对同样的输入换掉a和b的顺序输出应该一样。这种性质不需要参考模型天然就是对的适合做二次确认。再比如分配律(a c) * b应该等于a*b c*b。把这类恒等式写成property等于让引擎从另一个角度证明DUT不是“恰好做对了某一个测试向量”而是“本质上算对了乘法”。4.2 约束的编写原则与常见陷阱约束写得好不好直接决定验证能不能收敛。写约束的核心原则是只限制输入空间不限制实现细节。比如乘法器有一条从DMA过来的总线你只关心它在正常模式下工作那么约束就可以写“模式选择信号只能等于NORMAL”。你千万不要去约束“不管模式信号怎么变输出都应该等于正常模式的结果”。这是把实现细节写进了约束里会让引擎得到一个自相矛盾的空间它会花大量时间试图分析永远不可能发生的情况。另外JasperGold的约束默认是“软约束”还是“硬约束”取决于你写的语句形式。assume property是硬约束引擎必须严格满足restrict在某些场景下会被放宽。对于输入约束我基本都用assume property确保引擎探索的每个状态都符合接口协议。还有一个老生常谈但每次都有人犯的问题不要约束复位行为。很多人会顺手写一句“复位期间输出等于0”这本身没错但如果你把复位期间的输出也加进了断言比较的窗口就会让形式化验证变得非常棘手因为它要额外证明“复位和复位释放”这些边界状态下所有信号都是正确的。更干净的做法是用disable iff (!rst_n)把复位期间的检查直接关掉让引擎只关心功能正常时的行为。约束里还有一个陷阱——过度约束导致漏检。比如你假设“输入的三位只可能是3、5、7”引擎确实不会去算输入为1、2、4、6的情况自然也就验证不到那些情况下的错误。如果需求文档本身没有这个限制这个约束就是在帮RTL“藏bug”。所以每条约束都要能追溯到需求写完之后自己过一遍这个限制是真实世界里的物理限制还是我为了省事加上的假设4.3 覆盖率的写法和作用不要以为formal验证就不需要覆盖率了。JasperGold也支持cover property用来证明“某个场景在数学上是否可达”。对乘法器而言覆盖率的重点不是“我测了多少种输入组合”而是“我想让引擎证明某个关键条件确实能被触发”。比如你想确认“累加模式下输出有可能出现最大值”——这不是断言要证明的性质但你希望DUT真的存在这样的路径。用cover propertyproperty c_max_product; (posedge clk) disable iff (!rst_n) (en valid (a 1) (b 1)) |- ##[1:3] (product 1); endproperty cover property (c_max_product);跑完prove -property c_max_product如果工具返回“COVERED”说明这个场景确实可以发生。如果返回“UNREACHABLE”你就得回头查约束是不是写死了或者DUT本身就不可能输出全1。这个信息对验证完备性判断非常有用。5. 实战流程编译、证明与收敛调优5.1 从源码到第一个证明结果我习惯用脚本来驱动JasperGold而不是每次都敲命令。Tcl脚本大概长这样# run_jasper.tcl set DESIGN_NAME multiplier_top set TOP_MODULE multiplier_top set FORMAL_TB formal_multiplier_tb # 编译文件列表 read_file -format sverilog { ../rtl/multiplier_top.sv ../rtl/multiplier_core.sv ../formal/formal_multiplier_tb.sv ../formal/formal_bind.sv } elaborate -top $TOP_MODULE # 设置时钟和复位 clock clk reset -expression !rst_n # 设定证明时间上限 prove -property p_product_valid -timeout 30m第一步编译第二步elaborate第三步设时钟弄复位第四步prove。一个16位的无符号乘法器如果RTL写得不夸张JasperGold在几分钟内就能给出证明结果。32位无符号乘法器也通常能在这个数量级内完成。真正需要调的是符号位、流水线级数多、位宽超过64位这种场景。跑完之后你一定会在session log里看到几类结果PROVED断言被证明在所有可达状态下成立这是最理想的结果。FAIL引擎找到了反例。不要慌先看反例波形八成是约束或者时序窗口写错了。INCONCLUSIVE/TIMEOUT引擎在限定时间内没跑完。这不代表DUT错了往往是证明策略需要优化。UNKNOWN/ABORT通常是因为某个assume写得太宽导致状态空间太野引擎提前放弃。5.2 证明跑不动时的调优手段这是这个项目最需要沉淀经验的地方。乘法器位宽从32位翻到64位时如果你直接傻跑大概率会超时。我常用的几种调优手段按性价比排序如下第一种使用-effort或引擎切换。JasperGold支持不同证明引擎比如基于SAT的-engine jasperproof、基于BDD的-engine bdd。乘法器这种纯数据通路的模块SAT类引擎通常表现更好但也不是绝对。BMC引擎适合看特定深度内的行为。先用小位宽确定哪个引擎对你这个DUT最友好再上大批量任务能省很多时间。第二种抽象和cut point。引擎在证明大位宽乘法器时内部会尝试自动做抽象。你也可以手动指定某些信号作为cut point比如把部分积的中间位切掉让引擎分步证明。这一步操作需要你对RTL数据通路有理解。手动cut point的风险是你切掉了某些对证明必要的逻辑导致断言变成“证明了一个简化后的不相关模型”从而产生假证明。我一般只在自动模式实在收敛不了时才手动介入。第三种case split——写多条property去拆位宽。比如64位乘法器你不要一下子证明整个64位对不对而是分别证明低32位结果正确、高32位结果正确用带[31:0]和[63:32]切片做比较。引擎分别处理每个子命题的难度比处理整个命题低好几个量级。最后再证明一次“高低位拼接等于完整结果”。这个方法我在多个项目里屡试不爽。还有一个很朴素但有效的调整是把prove的timeout往上加。不要动不动就设5分钟发现没跑完就说“工具不行”。JasperGold官方文档里多种引擎的推荐跑法是一小时到几小时不等。当然如果你的迭代周期很紧每次改代码都要当天出结果那设置-timeout 2h在连续回归里跑着第二天早上看结果是合理的节奏。5.3 反例分析的实操技巧FAIL之后最重要的工作是搞清楚这是RTL的bug还是验证环境的bug。我这几年看到的比例大概是“环境问题占六成RTL真bug占四成”。所以别急着改RTL先看反例。JasperGold生成反例之后会在GUI里给出一个波形和原理图。你重点关注三个点一是反例输入的a和b是什么值。如果出现了你约束里没限制的边界值比如满位宽全1、0、符号位极值那很可能就是RTL真正漏算的边界情况恭喜你抓到一个真bug。二是看输出到底在哪一拍变了。用##[1:3]这种窗口时引擎找的反例往往是“输出在第三拍才有效而断言期望第二拍”。这种反例就是一个纯粹的时序窗口配置问题把range改成##[1:4]或者##[2:3]问题就没了。三是看反例路径里有没有出现不可思议的中间状态。比如输入明明被约束成只能取偶数值反例里却冒出个奇数。这说明约束没生效——检查一下assume property是不是写在了没有被elaborate到的模块里或者时钟域没对齐。这类问题很隐蔽我第一次遇到时排查了整整一个下午。有些老的JasperGold版本生成反例后会自动把反例存成.fsdb或.vcd文件供第三方工具打开。如果你习惯用Verdi看波形那就在脚本里加一句record_trace -vcd方便把trace导入到更熟练的环境里去分析。6. 源码获取与二次开发建议标题里提到[源码]说明大家关心的不只是方法更关心能直接跑的代码从哪来、怎么用。项目里的源码我建议你按“RTL Formal TB Scripts”三件套来获取和整理。Verification Academy、Cadence官网的技术论坛、以及GitHub上搜jaspergold formal multiplier都能找到可参考的样例工程很多EDA厂商的应用工程师也会在分享时放出配套代码。拿到源码之后不要直接拿来就交差。正规的做法是第一步先做“空白跑通”即原封不动编译、prove一遍确认默认配置下能出结果记录它的断言数量和证明耗时建立基线第二步“改造约束”把源码里跟你的DUT接口不匹配的信号名、位宽、时序窗口全部改成你项目的参数第三步“加料”加入你自己需求里的特殊模式比如溢出标志位输出、饱和处理、符号扩展位行为。这里有必要提醒一个常见的坑网上下载的formal源码经常省略了时钟和复位的声明或者默认你会在run.tcl里用clock命令指定。如果你编译报“no clock defined”不要以为源码有问题先看脚本这通常是环境问题而不是代码问题。另外一个坑是源码里的parameter可能和你的DUT实际位宽不一致elaborate之后会报位宽不匹配的warning别忽略这些warning直接看是不是parameter没覆盖到。迭代开发时我建议把脚本参数化。比如用Tcl变量控制位宽、是否启用符号模式、是否启用累加模式set WIDTH 32 set SIGNED_MODE 1 if {$SIGNED_MODE} { set TB_PARAMS $TB_PARAMS -parameter formal_multiplier_tb::SIGNED_MODE 1 }这样你改参数不用动RTL只动脚本回归管理也轻松。最后一个经验分享验证代码的review和RTL代码的review同等重要。正式提交formal testbench的时候拉上你的同事或者mentor把每条assume、每个assertion都口头解释一遍这是干嘛的。解释不清楚的地方大概率就是有问题的。形式化验证的产出物是“证明”但证明的正确性取决于property的正确性如果property本身写错了工具给你报一个PROVED反而是最危险的结果——因为所有人都以为验证过了实际上啥也没验到。我用了很长时间才真正理解这句话的分量。以我个人的实际操作体会来说JasperGold验证乘法模块这个需求真正难的部分从来不是工具语法而是你能不能把自己的验证意图用数学语言讲清楚。每次拿到一个新的乘法器设计我会先花一整个下午在纸上推演接口协议、边界情况和参考模型而不是急着敲代码。这个习惯帮我省下的时间远远超过写代码本身的时间。至于源码记得养成标注版本的习惯——RTL改了formal testbench必须跟着同步更新版本对不上验证结果就是废纸。本文还有配套的精品资源点击获取