简介一份面向数字IC验证工程师和EDA工具学习者的源码包提供了一套基于JasperGold形式化验证平台的完整乘法器验证工程。工程围绕Booth算法乘法模块展开覆盖从输入输出信号与握手信号定义、时钟复位配置到C黄金参考模型搭建、TCL验证脚本编写再到virtual_net简化RTL逻辑、proof_structure管理验证步骤的完整流程。资源共7个文件除Verilog顶层模块、C黄金参考模型、TCL脚本和Markdown说明文档外还包含辅助配置与忽略规则文件压缩包仅9KB轻量便于快速部署验证环境。目前已有131人学习适合需要掌握JasperGold断言添加、分支断言处理及验证空间优化技巧的读者。通过研读源码和脚本能够直接复用黄金模型与TCL自动化流程结合文档中的技术细节梳理可有效缩短自身验证环境的搭建与调试周期也可为其他算术单元的验证提供方法参考。1. JasperGold验证乘法模块仿真测不到的乘法边界formal十分钟就能抓出来乘法模块看起来是所有IP里最简单的一类仿真时功能覆盖率跑满、随机激励撒下去几千个cycle谁都觉得这模块稳了。可真正把芯片送回来后往往是一个符号扩展位没接对、一个多拍流水线没对齐让整条数据通路算错而不自知。JasperGold这种formal验证工具把“验证乘法模块”这件事从抽样测试变成数学证明不需要制造几亿条激励而是用求解器把输入空间剪枝后穷举证明再结合源码和SVA断言逐条check。这篇文章围绕“JasperGold验证乘法模块[源码]”展开从拿到RTL源码开始讲清楚性质验证怎么做、断言怎么写、约束怎么设、prove跑不动了怎么办。适合正在写verification plan、被乘法边界bug折磨或者第一次要把formal落到真实项目的验证工程师和设计工程师。2. 乘法的形式验证先分清要证什么再决定用什么引擎2.1 乘法器为什么适合用formal数据通路的边界不是靠随机激励碰出来的乘法器是典型的纯数据通路模块控制逻辑很浅甚至没有。常见的输入是两个带符号或无符号的N位操作数输出是2N位的乘积最多再加个valid握手。这类模块在仿真里的验证成本并不低如果做随机仿真两个16位操作数的组合空间是2的32次方仿真器能采到的样本在这个空间里稀疏得可怜。边界问题比如负乘负、最大值乘最小值、位宽截断后的符号扩展往往长期潜伏在覆盖率报告之外。JasperGold的引擎会把属性断言转成可满足性求解问题对输入空间做数学上的穷举分析。它不依赖你“有没有想到”哪条边界而是只要约束条件允许求解器就会去尝试找反例。这个性质让乘法器成为formal验证最典型的落地场景之一数据通路逻辑明确、状态少、结果可参照非常适合用断言直接约束输出关系。我在实际项目中接触到的乘法模块bug几乎都不是随机仿真能跑出来的而是集中在几个固定模式有符号数扩展位写错、乘法结果截断时符号位丢失、流水线握手信号错位导致采样到半成品数据。这些bug的共同特点是你很难靠“多跑一会儿”发现但形式验证可以在几十秒内给出falsified反例。这就是为什么我拿到乘法模块的第一反应是走formal而不是再开一轮仿真回归。提示如果你的测试bench已经把功能覆盖率跑到100%但审查时心里仍不踏实乘法模块正是formal能补上这块心病的地方。2.2 性质验证与等价性验证两条主流路线的适用边界与选型理由JasperGold上验证乘法模块有两条路线可选。第一条叫性质验证property verification用SVA断言描述乘法模块的行为属性比如“当valid拉高后输出应该等于输入的乘积”然后由formal引擎对输入空间做穷举证明。第二条叫等价性验证equivalence checking把实现和参考模型做逐拍比对通常是RTL对RTL、或RTL对门级网表用来确认综合、插DFT、retiming之后电路行为没变。选哪条取决于你的验证目标。如果是在设计早期确认乘法器满足规格比如溢出标志、饱和策略、符号位处理是否符合预期或者模块里包含流水线和握手逻辑需要按拍验证选性质验证。如果设计已经综合完成想知道网表有没有被工具改坏或者想知道某个优化选项是否改变了行为选等价性验证。很多乘法IP的验证计划会两条路线都上功能正确性用性质验证网表一致性用等价性验证。对比项性质验证等价性验证验证对象RTL行为属性RTL与参考模型/网表断言来源SVA手写或断言IP自动比对逻辑关心的问题功能规格对不对实现是否等价收敛难度与属性和约束相关与逻辑锥深度相关典型场景乘法器溢出、符号、握手综合后网表确认、retiming检查从标题“验证乘法模块”的角度看我一般默认先做性质验证因为乘法器的验证本质是回答“这个模块算得对不对”而性质验证能直接回答行为正确性等价性验证往往放在流程后半段。我们的源码工程也会按照这个思路组织RTL源码旁边放SVA断言文件和JasperGold批处理脚本而不只是套一个仿真testbench了事。2.3 拿到源码工程先读四样东西验证目标、端口、时钟复位、已建约束不管源码是你自己写的还是从别处拿来的先别着急打开JasperGold跑命令。常见做法是先在源码目录里做一轮静态阅读确认四件事验证目标是什么、端口信号完整与否、时钟复位关系、有没有已经写好的约束或断言文件。验证目标决定你要建性质还是做等价比对端口信号决定SVA能否对齐采样时序时钟复位决定disable iff怎么写已有约束决定了你是增补还是重写。这份源码工程我通常组织成这样的布局RTL文件放rtl目录、SVA属性文件放verify目录、JasperGold脚本也放verify目录。RTL文件先确认乘法器是纯组合逻辑还是带流水线寄存器输出有没有valid伴随信号复位是高有效还是低有效。这些信息直接决定断言的形式组合输出用“当前拍比对”寄存器输出用“下一拍比对”流水线输出则要按延迟拍数对齐。刚接触formal的同事经常在这步跳过去直接看代码逻辑结果在JasperGold里elaborate完才发现时钟复位信号没连对prove出来的结果全是垃圾。我的习惯是先在代码里搜三个关键字always_ff、assign、valid把数据通路和控制通路的边界画出来再决定property从哪个信号下手。这一步做完后面写断言和约束基本就是填空。3. 在JasperGold上跑通乘法模块验证从源码到第一个proven3.1 工程目录结构RTL与验证文件分离的落地布局一份可回归的formal验证工程文件组织比大多数人想象的重要。我一般会按下面这个结构组织源码和验证文件RTL和formal文件严格分开避免混在一起让elaborate误读mul_verify/ ├── rtl/ │ ├── mul_core.sv # 乘法器RTL组合乘法 输出寄存器 │ └── mul_pipeline.sv # 流水线乘法器参数化LATENCY ├── verify/ │ ├── mul_assertions.sv # SVA属性交叉验证断言 │ ├── mul_env.sv # 输入约束valid、reset时序 │ └── mul_engine.tcl # JasperGold批处理脚本 ├── work/ # 工程目录run之后生成 └── run_mul.sh # 一键回归脚本把断言和约束拆成两个文件是因为它们生命周期不同断言表达了设计规格基本稳定约束表达了验证环境的边界经常要调整。而且JasperGold在elaborate时会把断言和RTL一起编译进去分文件更方便读报告时定位问题。run_mul.sh里就一句话调用jgc跑批处理脚本。这样每次RTL改动或约束更新后整个回归可以无脑重跑。提示work目录是JasperGold生成工程数据的地方里面的内容不要手工改。我见过有人为了调约束直接改work下的工程文件结果下次run时整个数据库损坏只能重新new_project。3.2 写第一条SVA断言交叉验证参考模型的做法与输入约束乘法模块验证里最可靠、也最适合新手上路的做法是在RTL内部做一个参考乘法器然后断言它和正式输出的结果逐拍一致。这种交叉验证的好处是参考模型和被测实现共享同一份输入不需要在断言里手工计算乘积也就避免了SVA表达式里运算符位宽扩展带来的坑。// rtl/mul_core.sv module mul_core #( parameter int WIDTH 16, parameter bit SIGNED 0 )( input logic clk, input logic rst_n, input logic valid_in, input logic [WIDTH-1:0] a_in, input logic [WIDTH-1:0] b_in, output logic [2*WIDTH-1:0] y ); logic [2*WIDTH-1:0] ref_y; // 主乘法通路输入有效时锁存乘积 always_ff (posedge clk) begin if (!rst_n) begin y 0; end else if (valid_in) begin y a_in * b_in; end end // 交叉验证参考模型与主通路完全相同的采样条件 always_ff (posedge clk) begin if (!rst_n) begin ref_y 0; end else if (valid_in) begin ref_y a_in * b_in; end end endmodule主通路的y和参考ref_y的采样条件保持一致都在valid_in为高时锁存位宽都是2*WIDTH。这样写出来的断言本质上是在验证“两条独立但行为相同的通路是否永远一致”它能抓出综合工具插入的额外逻辑、手工修改导致的位宽截断、甚至寄存器被误优化掉的问题。// verify/mul_assertions.sv module mul_assertions; // 交叉验证主输出和参考模型必须逐拍一致 ap_mul_ref : assert property ( (posedge clk) disable iff(!rst_n) valid_in | y ref_y ) else $error(mul_core: y mismatch ref_y); endmodule这里用的是蕴含算子|含义是“valid_in为高的下一拍检查y和ref_y相等”。之所以写下一拍是因为y和ref_y都是时钟沿采样的寄存器输出采样后的第一个稳定周期才是可比对的时间点。如果写成组合断言会比较当前组合逻辑的毛刺formal会给一堆无意义的falsified。每条断言后的else分支可以让仿真和formal共用一个断言文件仿真挂failure时也更容易定位。3.3 JasperGold批处理脚本最小命令流与参数说明JasperGold可以用图形界面逐条敲命令但要做成可回归的验证资产批处理脚本是必须的。下面是我常用的最小脚本足够把一个乘法模块的验证跑完并输出报告。# verify/mul_engine.tcl set DESIGN mul_core set RTL_DIR ./rtl set ASSERT_DIR ./verify new_project -name mul_prj -work ./work read_file -format sverilog [list \ $RTL_DIR/mul_core.sv \ $ASSERT_DIR/mul_assertions.sv] elaborate -top $DESIGN -disable_simulation clock clk -period 10 reset rst_n -active low assume -name valid_always -env { valid_in 1b1 } -after 2 prove -all -timeout 600 report -summary write_report -dir ./report命令很直白new_project创建工程目录read_file把RTL和断言文件一起读进来elaborate指定顶层模块。clock和reset约束告诉形式验证引擎时钟周期与复位极性这是prove能收敛的前提。assume这里把valid_in固定为1是因为本例中我们只关心乘法结果本身握手逻辑另开property验证。-prove -all会把当前design里所有未证明的属性一起跑-timeout 600表示每个属性最长跑600秒。实际项目中我习惯先把timeout设成60秒跑一轮看哪些属性方向不对而不是一上来就给1800秒否则等半天发现断言写错浪费一整个下午。write_report会把断言报告、覆盖率数据、疑似不可达状态统统导出方便以后review。脚本写完后在terminal里直接调用JasperGold的命令行入口运行jgc -project mul_prj -run verify/mul_engine.tcl第一次跑通时大概率不会直接给你proven而是先冒出一堆语法问题、断言格式错误。这时候别慌JasperGold的报错日志基本会把具体哪一行哪个token有疑问写清楚对着改就行。等真正跑通后把这条命令写进回归脚本之后每次改动RTL只需重复执行不需要再开图形界面。3.4 读证明报告proven、falsified与undetermined的下一步prove跑完后report -summary会列出每条属性的状态。第一个值得开心的状态是proven意味着formal引擎在约束允许的输入空间内完成了穷举证明这条性质在数学意义上是成立的。第二个状态是falsified说明引擎找到了反例从反例波形里能看出具体是哪一拍、哪个输入组合导致失败。第三个状态是undetermined意味在timeout内没跑完通常是设计太大、约束不够、或者断言写得让引擎很难收敛。看到falsified先别急着改RTL。最常见的情况是约束没有给到位比如valid_in在真实场景里不会连续拉高但你在环境里允许了所有组合于是引擎构造了一个“真实设计里不会出现”的序列把断言打穿。正确顺序是先看反例波形确认这个反例在真实环境中是否可达如果不可达就去加强约束如果可达才说明RTL有真bug。看到undetermined相对麻烦说明这个属性当前约束、引擎配置、设计复杂度下没能在限定时间内证完。这时候需要检查是不是位宽太大、参考模型创建了过大的逻辑锥或者考虑用第4章讲的分块策略。手动把timeout从600秒加到3600秒往往是最下策收敛不了一样收敛不了反而是约束写得越精准prove收敛越快。4. 乘法模块验证收敛位宽、符号、流水线与分块交叉验证4.1 位宽与符号SIGNED参数引发的断言差异与符号扩展典型bug乘法模块最常见的翻车点不在乘法本身而在位宽和符号的边界处理。16位无符号数相乘结果是32位这没有争议但如果输入是signed类型两个16位有符号数相乘结果可能只需要31位有效数据但位扩展错了就会在最高位留下错误符号。JasperGold里prove出来的反例往往就是这个某个极端输入组合下输出比参考模型少一位或符号位错误。// 带符号控制的乘法通路 module mul_signed #( parameter int WIDTH 16, parameter bit SIGNED 1 )( input logic clk, input logic rst_n, input logic [WIDTH-1:0] a_in, input logic [WIDTH-1:0] b_in, output logic [2*WIDTH-1:0] y ); logic signed [WIDTH-1:0] a_s; logic signed [WIDTH-1:0] b_s; assign a_s SIGNED ? $signed(a_in) : $signed({1b0, a_in}); assign b_s SIGNED ? $signed(b_in) : $signed({1b0, b_in}); always_ff (posedge clk) begin if (!rst_n) y 0; else y a_s * b_s; end endmodule这里的做法是先把输入统一转成signed再做乘法。无符号输入通过前置0扩展到signed域确保位宽和符号语义一致。这个代码里最容易出错的是$signed({1b0, a_in})和直接$signed(a_in)的区别如果a_in本身最高位是1直接$signed会把最高位当作符号位把无符号数错判成负数乘积符号就反了。断言层面也要配合SIGNED参数做区分。我习惯在assertions文件里用generate块分别例化有符号和无符号的断言或者用一个宏控制$signed()的包裹对象。很多教科书示例没有这一步直接拿logic vector做比较formal引擎会按无符号语义处理于是仿真pass但formal报falsified查半天发现是断言语义错了RTL反而没问题。所以写属性时脑中必须有一张表输入是有符号还是无符号、输出是否扩展到2倍位宽、比较表达式里两边有没有同样的符号性。4.2 流水线乘法器延迟拍数与信号对齐策略实际IP里的乘法器很少是纯组合逻辑大多带有流水线寄存器常见的是两到三级。流水线的引入改变了断言的时序关系valid_in拉高后输出不是下一拍就能采到而是要在LATENCY拍之后。很多人第一次写流水线乘法器的断言时直接用valid_in | y ref_y结果falsified原因就是y还在流水线里没出来ref_y已经提前更新了。// rtl/mul_pipeline.sv — 参数化延迟的流水线乘法器 module mul_pipeline #( parameter int WIDTH 16, parameter int LATENCY 3 )( input logic clk, input logic rst_n, input logic valid_in, input logic [WIDTH-1:0] a_in, input logic [WIDTH-1:0] b_in, output logic [2*WIDTH-1:0] y, output logic valid_out ); logic [2*WIDTH-1:0] mul_stage [LATENCY]; always_ff (posedge clk) begin if (!rst_n) begin for (int i 0; i LATENCY; i) mul_stage[i] 0; valid_out 1b0; end else begin mul_stage[0] a_in * b_in; for (int i 1; i LATENCY; i) mul_stage[i] mul_stage[i-1]; valid_out valid_in; end end assign y mul_stage[LATENCY-1]; endmodule对于这类设计我一般不尝试在断言里用$past(a_in, LATENCY)去对齐。原因很简单LATENCY如果是参数$past的第二个参数必须是常量参数化断言写起来很别扭另外一旦流水线内部有气泡或背压纯按固定拍数对齐很容易错位。更稳的做法是让参考模型也变成同等拍数延迟的移位链路然后比较y和ref_y在同一个delay下的结果断言valid_out | y ref_y。另一个常见做法是使用valid_out信号做对齐valid_out拉高那一拍y才是有效结果断言只在valid_out有效时比较。这样就把“延迟几拍”的复杂度从断言里剥离了流水线改动时只需保证valid_out时序正确。等价性验证里也是类似的逻辑JasperGold会把valid_out当作数据有效标志由它选通比较窗口而不是靠固定拍数硬对齐。4.3 大位宽乘法器的分块与约束当prove跑不动的实用降级方案64位乘法器直接做性质验证引擎的解空间会大得吓人prove经常跑到undetermined。这时候不能硬扛而是要分块。我常用的做法是把大乘法拆成子块乘加结构64x64拆成4个32x32再把32x32拆成4个16x16对每个子块单独做性质验证最后在顶层只验证子块间的连接和累加逻辑。分块验证的价值不只是降低求解难度还能精准定位问题顶层falsified时根据反例追到哪个子块输出不对直接去查那个子块的断言调试范围缩小一个数量级。代价是需要额外维护子块参考模型和顶层约束工程量大一些。更适合的做法是先用JasperGold跑一遍全位宽如果undetermined再分块不要上来就拆。还有一种折中方法对有问题的输入空间做约束剪枝。比如只在乘法器的高位做边界分析时把低位输入约束为0或固定值。这个做法必须非常小心因为约束过强会让proven失真——你证明了“低位全0时高位正确”但真实场景里低位是随机数据说不定高位进位正是bug来源。我一般只在探索阶段用这种约束做快速定位最终结论还是以不剪枝或弱剪枝的证明为准。策略适用场景风险全位宽直证位宽32属性简单位宽增大后可能超时子块分块验证64位以上大乘法器子块接口抽象成本高输入空间剪枝快速定位问题约束过强导致误报proven等价性验证补充综合后网表确认不验证功能规格5. JasperGold验证乘法模块的避坑记录五个绕不开的坑5.1 环境脚本不生效elaborate时报systemverilog语法不支持现象elaborate时报出一堆语法错误比如interface、struct、2-state类型无法识别或者read_file时直接跳过部分文件。原因多半不是代码语法问题而是JasperGold的仿真器/编译环境变量没配对。形式验证引擎在elaborate阶段会调用配套的仿真器解析SystemVerilog如果环境下默认的仿真器版本过旧或者license不支持新语法再好的代码也读不进去。解决先确认当前shell环境里JasperGold的setup脚本已经source过再确认read_file里指定的-format是sverilog而不是verilog。还不行就在elaborate前手动指定工具链版本比如setenv或module load对应版本。我在这类问题上吃过亏后来干脆把环境初始化写进run脚本的第一行每次run前强制source一遍从源头消除“环境没配好”这个变量。5.2 约束过弱导致prove被falsified反例来自“输入根本不会出现”现象断言报falsified打开反例一看输入序列是valid_in连拉了几十拍不落、或者a_in在reset期间就有变化。这些波形在真实设计里根本不可能出现但你忘了告诉引擎。形式验证的引擎是“没有约束就认为什么都可能”这是它和仿真的本质区别仿真激励有testbench管着formal没有必须由你主动画边界。解决逐一检查assume约束把复位期间的有效信号、valid_in的拉高条件、输入信号的置位时机全部显式声明。比如复位释放后的前两个cycle不允许valid_in拉高就用assume加上时间条件如果乘法器只在使能信号为高时接受输入就把使能条件写死。这项工作没有捷径只能对着反例波形一条条补。补完后再重新prove通常会从falsified变成proven。5.3 约束过强导致proven是假象覆盖率报告里的unreachable要看见现象prove全部proven但验证报告里的coverage显示某些输入组合unreachable或者某条分支永远没被探索。这比falsified更危险因为它会让你误以为设计安全。原因几乎都是assume写得过于激进把真实会出现的输入给排除掉了。一个典型例子为了收敛快把a_in限制在0到255之间但设计规格允许a_in有符号负数负边界在证明中被绕开了。解决每次拿到proven报告花两分钟看一眼unreachable coverage。尤其确认输入范围是否覆盖规格上下限、valid握手是否能拉低再拉高、复位序列是否正常。我习惯在约束文件里给每条assume注明来源写清楚这条约束是出于硬件限制还是为了收敛。如果是为了收敛而加的必须在最终版本里拿掉。形式验证最忌讳的玄学问题就是“约束里留下一个只为自己省时间的hole”最后带着hole上市。5.4 断言时序语义写错组合信号当寄存器信号比一拍之差全是误报现象断言本身逻辑没问题但总是falsified而且反例里看不出RTL哪里错输出和参考模型就差一排错开。原因几乎都是SVA时序算错了把组合输出当成寄存器输出对待、或反过来。比如纯组合乘法器的输出y是组合信号在时钟沿采样时看到的是当前输入组合的稳态值断言比较的对象和比较的拍位必须和RTL结构严格对应。解决先画RTL结构图标出哪些信号是组合的、哪些是寄存器输出再决定|-还是|。组合输出通常用|-和组合表达式直接比较寄存器输出要延迟一拍流水线输出要延迟LATENCY拍。另一个有效技巧是用default clocking让所有断言统一对齐一个时钟域避免多个属性因时钟选错产生时间偏移。这坑基本靠代码走查和完整时序分析避免没有等价工具替代。5.5 综合后网表等价失配黑匣子DSP硬核成了压垮骆驼的最后一根稻草现象RTL的formal验证全proven但综合后网表和RTL做等价性验证时乘法器相关的compare point直接mismatch。原因多半是综合工具把乘法器映射到了DSP硬核硬核的行为细节尤其是对溢出、rounding、饱和的处理和RTL中普通乘法运算符的语义不完全一致。JasperGold把DSP硬核当成黑匣子处理或者硬核本身有不支持的模式都会导致等价失配。解决先确认综合工具对乘法器的约束area/power优化是否把乘法重映射成不同结构再把网表中DSP硬核设置成dont verify单独对硬核做额外的行为确认。这部分很难自动化我习惯在项目早期就和综合工程师约定好乘法器IP的边界由谁验证、RTL里哪些乘法运算符是黑匣子、哪些必须全程透明。如果RTL乘法器最终会被综合成DSP硬核最好一开始就把硬核行为模型写出来formal和仿真共同用它。6. 把prove结果变成可回归的功能验证资产覆盖率量化与约束回归验证做完prove只是第一步把结果变成团队能长期依赖的资产才是这次投入真正值回票价的地方。JasperGold跑完prove后不要关掉页面就完事先做两件收尾工作一是把覆盖率数据导出二是把约束和断言固化为回归脚本的一部分。覆盖率数据能告诉团队哪些输入空间是被数学证明覆盖的哪些没有被任何证明触及。这个数据可以喂给下游的功能验证计划让动态仿真的回归测试集中在formal覆盖不到的区域两个验证手段形成互补。约束回归是我踩过坑后养成的习惯。早期我做formal喜欢在图形界面里手调assume调通了就把工程放着不管。结果三个月后RTL改了一版重新跑formal时发现约束文件里的时钟结构和新RTL对不上整个验证环境报废重新调试花了两周。现在我把所有assume写在mul_env.sv里和RTL源码一起进版本库每次提交RTL变更都触发一次formal回归如果新增逻辑影响乘法通路回归会立刻暴露如果约束里写明了设计边界review代码的人也能直接看到验证环境的假设而不是对着二进制工程文件猜测。最后的具体技巧是把关键断言拆分成更细粒度的property每个property只回答一个明确的验证问题。比如“y与ref_y一致”这条断言我会拆成“无符号输入下y与ref_y一致”“有符号输入下y与ref_y一致”“复位后首个有效输入y与ref_y一致”三条独立property。这么做的好处是回归失败时能直接定位到是哪类输入场景出了问题而不是面对一条综合断言发愁。这个习惯在后续IP演进中救过我很多次现在每跑一次乘法模块的formal回归我都会顺手把每个property的prove时长和状态记录在验证报告里作为下次优化的基线。希望帮到你。本文还有配套的精品资源点击获取