简介一份面向数字IC验证工程师及学习者的JasperGold形式化验证入门源码包聚焦基于Booth算法的乘法器模块验证。资源内含RTL设计文件、C黄金参考模型、TCL自动化验证脚本及说明文档完整呈现从模块信号定义、时钟复位配置、断言添加到利用virtual_net与proof_structure优化验证流程的实用思路适合希望快速上手JasperGold工具或参考形式化验证流程的开发者。压缩包共7个文件以markdown文档、TCL脚本、C模型和Verilog源码为主另有辅助配置文件总体积仅9KB结构紧凑便于对照学习。目前已有126人学习下载。通过该资源可掌握乘法器验证环境搭建、C模型准备、断言编写与验证空间优化等关键技巧为自身项目中的复杂模块验证提供可直接借鉴的工程模板。1. 为什么我用JasperGold来验证乘法模块做IC验证的同行对JasperGold应该都不陌生它是Cadence家的形式验证工具在等价性检查、属性证明、死锁检测这些场景里表现非常稳。我最近完整地做了一次基于JasperGold的乘法模块验证从拿到RTL源码到跑通全部property中间踩了不少坑也想清楚了很多以前没细琢磨的点。这篇就把整个思路、源码级操作、prove过程和一些排查经验完整记录下来对有同样需求的人应该有点参考价值。先说说为什么拿JasperGold来验证乘法模块而不是继续堆UVM仿真。乘法器这种东西本质上是纯组合逻辑函数给它两个操作数输出就是确定的乘积。理论上你要验证的功能非常清晰——输出必须等于两个输入相乘的数学结果。但麻烦在于乘法器为了实现高性能内部架构千奇百怪有Booth编码加Wallace树的有Dadda压缩器的有流水线打拍的还有带饱和截断和符号扩展的。这些结构一旦展开全加器阵列的规模会迅速膨胀如果用仿真随机激励去撞你会发现自己撞到的只是巨量输入空间里极小一部分很多边界进位、符号位扩展、溢出截断的问题是根本测不到的。JasperGold走的是另一条路——形式化穷举。它把RTL建模成有限状态机把你要验证的属性写成断言然后在数学上搜索整个状态空间看是否存在违反属性的路径。对乘法模块这种结果可预测的逻辑形式验证的适用性几乎是天然的。你不需要生成上百万条激励只需要把“输出等于两个输入相乘”这个属性写出来剩下的交给求解器去证明。我当时接手的乘法模块是32位的有符号定点乘法器带三级流水线输出还做了饱和处理。刚开始我确实有点怵因为参与验证的同事反馈说之前用UVM跑回归覆盖率做到95%以上了还是被验证的同事挑出来几个进位链上的漏测点。换用JasperGold之后我最大的感受是仿真验证和形式验证根本不是替代关系而是两种不同维度的手段。仿真是在有限样本里抽样检查形式验证是在整个数学空间里证明或找反例。对乘法模块这种纯函数型逻辑形式验证效率反而更高。2. 乘法模块源码梳理与验证目标定位2.1 从源码中识别行为级属性和结构级属性拿到乘法模块的RTL源码之后第一件事不是急着写property而是把源码从头到尾过一遍搞清楚这个乘法器到底是什么结构、有没有流水线、有没有独立的时钟门控、复位方式是什么。我拿到的那份代码大概是这样的结构module multiplier_32 ( input logic clk, input logic rst_n, input logic valid_in, input logic [31:0] a, input logic [31:0] b, output logic valid_out, output logic [31:0] result ); logic [63:0] partial_product; logic [31:0] a_reg, b_reg; always_ff (posedge clk or negedge rst_n) begin if (!rst_n) begin a_reg 0; b_reg 0; end else if (valid_in) begin a_reg a; b_reg b; end end // 组合乘法结果 always_comb begin partial_product $signed(a_reg) * $signed(b_reg); end // 流水线输出打拍 always_ff (posedge clk or negedge rst_n) begin if (!rst_n) result 0; else result partial_product[31:0]; //低32位输出 end endmodule这段代码简化了很多但足够说明问题。我需要验证的属性可以分成两类一类是行为级属性直接描述输入输出关系比如“对于任意输入a和b输出result等于a_b的低32位乘积”另一类是结构级属性比如“valid_out信号在valid_in有效后的第三个周期才有效”、“复位后输出归零”等等。行为级属性是乘法器验证的硬核部分也是JasperGold最擅长的地方。你写一个property把参考模型和DUT的输出做等价比较JasperGold会在所有可能的输入组合上尝试证明。这里有个关键点不要直接在property里用乘法表达式去比对因为如果RTL内部也是用乘法器实现的你等于把DUT和参考模型混在一起JasperGold的求解器可能会走捷径甚至在选择引擎时出现不利于证明的分析路径。更稳妥的做法是把参考模型抽象成独立变量或者用组合逻辑单独生成期望值然后断言DUT输出与之相等。2.2 参考模型怎么搭最不容易出错在JasperGold里参考模型的搭建方式直接影响证明难度和debug效率。我踩过的一个坑是把参考模型写得太复杂比如用了一个行为级的有符号乘法器加上一堆边界条件判断结果prove时间从几分钟暴涨到几个小时。后来我把参考模型简化成只有一行“a * b”再单独把符号扩展和饱和逻辑拆成几个辅助属性去验证整个证明过程快了很多。经验是参考模型要尽可能简单哪怕它看起来冗余。JasperGold的求解器对算术表达式是有内部优化策略的参考模型越贴近数学定义求解器越容易做等价变换。像乘法这种运算参考模型写成“$signed(a) * $signed(b)”比写成一个展开的移位加算法要快得多。另外如果乘法模块有流水线延迟参考模型也要跟着打拍对齐否则你写出来的属性在时间上永远对不齐prove会一直报fail。我当时把验证目标拆成了三个部分组合乘法核心a和b的64位乘积是否正确输出截断逻辑低32位输出是否等于完整乘积的低32位流水线时序关系valid_out相对valid_in是否为固定节拍延迟。拆开之后每个属性都变得很独立JasperGold可以针对不同属性选择不同的求解策略调试反例时也不会互相干扰。3. JasperGold验证环境搭建与核心配置3.1 工程初始化与文件加载JasperGold的工程搭建其实比很多人想象中简单。工具本身是在命令行下运行的你启动后先创建工程再读取设计文件。整个过程我会用一段典型脚本说明# 创建工程 create_project multiplier_verify # 设置顶层模块 set_top module multiplier_32 # 读取RTL源码 read_file -format sverilog -top multiplier_32 {multiplier_32.sv} # 如果需要读取网表或者库文件可以继续添加 # read_file -format verilog -top multiplier_32 {gate_lib.v}这里有个容易被忽略的点如果RTL里引用了某个IP或者子模块JasperGold并不会自动去网上一层层找文件你必须把依赖文件全部显式加载进来或者用“-incremental”属性让它按层次解析。第一次跑的时候我漏加载了一个小的时钟门控单元工具直接报找不到模块折腾了半天才意识到是文件列表不全。还有一个非常实用的选项是“elaborate”或者说你需要让工具执行一次详细的层次化展开它会检查模块端口对不对、信号宽度匹不匹配、有没有未连接信号。对于大型设计这一步能提前暴露很多连线问题。之前我见过有人在正式prove之前不做elaborate结果跑到一半发现内部信号名字写错了白白浪费几小时。3.2 时钟、复位与约束的常规处理JasperGold在prove之前需要你定义清楚时钟和复位行为。它不是仿真器不会自动从波形里推断出时钟周期你必须显式指定哪些信号是时钟、哪些是异步复位/置位。# 定义时钟 clock clk # 定义复位 reset -expression {!rst_n} # 对输入信号加约束 assume {valid_in 1}看到这里可能有人会问为什么要把valid_in约束为1因为对于纯数学的乘法验证我们希望工具在完整输入空间上去证明乘法器的正确性如果你把valid_in放开工具就会在valid_in为0的周期里探索那些不关心数据输入的路径白白浪费求解资源。当然这要结合设计语义如果valid_in为0时数据可以任意那我就在约束里把输入数据限定为随机任意值如果valid_in为0时有特殊的低功耗逻辑或保持逻辑那就需要额外分析。时钟复位处理上还有一个关键点JasperGold默认对异步复位会做全路径分析如果你的复位信号还牵扯到内部状态机的异步清零建议在约束里补充一句“-nonexist”之类的时序限定避免工具把复位置位路径也纳入正式证明范围造成不必要的复杂度。4. 断言编写与prove实战过程4.1 直接乘号属性 vs 参考模型属性写属性是JasperGold验证的核心动作。对于乘法模块最简单直接的方法是在property里直接对比DUT输出和表达式结果// 直接乘号属性 property p_multiply_result; (posedge clk) disable iff (!rst_n) valid_out |- (result $signed(a_reg) * $signed(b_reg)); endproperty assert property (p_multiply_result);这种写法直观但有个隐患——如果你RTL内部也是用“$signed(a) * $signed(b)”实现的那你等于拿参考模型的乘法器去验证同一个乘法器JasperGold的求解器虽然也能证明但它可能会直接走“同一表达式等价”的捷径万一你和参考模型在符号宽度或中间精度上理解不一样反而掩盖了真实的功能漏洞。更推荐的做法是显式构造一个独立的参考信号让这个参考信号只依赖原始输入不依赖DUT内部的任何信号logic [63:0] ref_product; assign ref_product $signed(a) * $signed(b); property p_multiply_correct; (posedge clk) disable iff (!rst_n) valid_out |- (result ref_product[31:0]); endproperty这样写的好处是参考信号是从端口a和b直接推导的不经过流水线寄存器也不受DUT内部状态影响。JasperGold在证明时会把参考信号树和DUT的数据通路完全隔离求解器可以更清晰地做算术等价判定。我实测下来这种写法在32位乘法器上比直接乘号属性平均快一倍左右。4.2 流水线延迟属性怎么写流水线结构的乘法器核心难点在于延迟对齐。我当时那个模块是三级流水线valid_out在valid_in后第三个周期拉起。如果你只写“valid_out为高时result等于当前输入的乘积”那肯定是错的因为在valid_out拉高那个周期a_reg和b_reg已经不知道被刷新多少次了。正解是把输入数据锁存到参考模型中并模拟同样的延迟周期logic [31:0] a_d1, a_d2, a_d3; logic [31:0] b_d1, b_d2, b_d3; logic [63:0] ref_product_d3; always_ff (posedge clk or negedge rst_n) begin if (!rst_n) begin a_d1 0; a_d2 0; a_d3 0; b_d1 0; b_d2 0; b_d3 0; end else if (valid_in) begin a_d1 a; b_d1 b; end end always_ff (posedge clk or negedge rst_n) begin if (!rst_n) begin a_d2 0; a_d3 0; b_d2 0; b_d3 0; end else begin a_d2 a_d1; b_d2 b_d1; a_d3 a_d2; b_d3 b_d2; end end assign ref_product_d3 $signed(a_d3) * $signed(b_d3); property p_pipeline_result; (posedge clk) disable iff (!rst_n) valid_out |- (result ref_product_d3[31:0]); endproperty这段代码看着啰嗦但逻辑很清楚参考模型的打拍方式必须和DUT完全一致。实际项目里DUT的流水线可能不是简单三级打拍而是输入级先做Booth编码、中间级做压缩、输出级做加法这时候你要在参考模型里也拆成同样的中间级否则时序对不齐。当然如果只是验证功能等价性只要保证“从端口输入到端口输出”的延迟周期一致就够了不需要把每个内部节点都复刻出来。4.3 prove执行与结果解读写完property后进入prove阶段。JasperGold的prove过程会在后台启动多个求解引擎你可以用一条命令发起全部属性的证明prove -all这条命令会把工程里所有assert property都跑一遍。跑的时候要注意看日志里面会显示每个property是“proven”还是“falsified”以及用掉了多少求解资源。正常情况下简单属性几秒到几分钟就能proven而如果设计很复杂求解器会尝试各种抽象和切割策略日志里也能看到它切换引擎的过程。第一次跑完我碰到了一种典型情况大部分属性都proven了但有一个“p_pipeline_result”始终被标记为“inconclusive”既没有证明也没有找到反例。这时候不要盲目加大求解时间而要先想想是不是自己的参考模型时序写错了。我当时检查了一圈发现是我参考模型里a_d1的刷新条件和DUT不一致——DUT在valid_in有效时才锁存输入但我的a_d1在任意周期都一直被赋值等于数据被提前刷新了。把这个问题修正后prove立刻通过了。5. 常见问题与排查技巧实录5.1 内存爆炸与超时的处理JasperGold虽然强大但面对复杂设计时也经常出现内存占用过高、prove超时的情况。我的经验是遇到内存爆炸先别急着调大服务器资源而是要检查是不是约束给得太松了。比如没有对valid_in加限制工具会把大量状态空间花在“valid_in为0”的路径上这些路径跟乘法正确性毫无关系。另外一个非常实用的选项是“范围抽象”。JasperGold支持对数据通路的某些位宽做抽象化处理比如把32位乘法分解成高16位和低16位分别证明或者用“cutpoint”把某些中间节点设为自由变量让求解器把注意力集中在剩余逻辑上。这需要你对设计结构足够了解找到合适的切割点否则抽象掉关键逻辑后prove出来的结果毫无意义。还有一种情况是属性本身写得太强。比如某些中间状态的低功耗逻辑、gated clock或者异步FIFO的控制信号并不适合用穷举方式证明。针对这类属性我会先把它标记成“assume”而不是“assert”只在特定条件下启用或者拆分成更小的子属性逐个验证。注意JasperGold不是万能的有些属性因为状态空间实在太大目前的形式化工具确实无能为力。千万不要天真地以为把所有property都prove过了就看不上仿真。实际项目中我都是JasperGold和UVM双轨并行JasperGold负责数学上可证明的属性UVM负责随机场景和场景交互逻辑。5.2 溯源counterexample的几个技巧如果prove报falsified工具会给出一个反例波形你可以在JasperGold的GUI里直观地看到从初始状态到违例状态的所有信号变化。我第一次遇到反例时手忙脚乱后来总结了一些快速的排查思路第一步先看反例发生时刻的输入a和b是多少用计算器验证一下DUT输出是否真的不符合数学期望。如果真的不符合那说明DUT有bug恭喜你仿真很久都没测出来的问题被形式验证一把抓到。如果DUT输出符合期望但property报falsified那多半是你的参考模型或时序对齐写错了。第二步看DUT内部的关键中间信号。比如我们那个乘法器我会重点检查partial_product高32位是否有值以及输出截断逻辑有没有把正确的位切出来。很多乘法器的功能bug其实不是乘法本身错了而是截断、饱和、舍入这些边界处理错了。第三步利用JasperGold的“reduce_counterexample”功能让工具把反例自动简化到最短长度。很多时候一个复杂的反例路径里大部分信号跳变对最终的违例没有任何影响。简化之后你只需要看几个关键信号的变化。5.3 一些更隐蔽的坑最后分享几个我在源码级验证中遇到的隐蔽问题这些问题在文档里很少被提及但实际踩到一次就够你难受半天。第一个坑是整数符号扩展。RTL里经常写“a[15:0]”取子字段然后直接参与乘法运算。如果不注意符号位扩展16位有符号数会被当成无符号数参与运算结果自然不对。这种问题在仿真里偶尔也能测出来但很容易被随机激励漏掉JasperGold的穷举能力在这里反而成了优势——它会在所有组合上验证任何符号扩展错误都会立刻暴露。第二个坑是并行case和full case。如果你的RTL源文件里写了“// synthesis full_case parallel_case”这种综合指令JasperGold在解析时可能会改变对case语句的语义解释。形式验证必须严格遵循RTL的仿真语义如果你在综合时用了full_case告诉综合器某些分支不会出现但在验证时又让工具把这些分支当作不存在那在某些输入组合下prove的结果就和仿真行为不一致了。遇到这种设计我会在JasperGold里用“-nosynthesis_case”之类的选项显式关闭综合语义或者简化case结构保证验证的语义和RTL仿真一致。第三个坑是复位后的初值。JasperGold在prove时会把复位释放后的初始状态作为探索起点。如果RTL里有寄存器没有在复位中被赋初值工具可能会认为它是一个自由变量导致证明结果覆盖了大量实际不会出现的状态。解决办法是在约束里给这类寄存器加上“init”或“assume”限定让工具按照实际复位行为来探索。还有一个非常实际的经验在跑大规模prove之前先建一个小位宽的乘法模块做个“smoke test”。比如把32位乘法器临时改成8位或16位版用同一套property快速地验证一遍流程是否顺畅。这能帮你提前发现环境配置、约束写法、时序对齐等问题免得在32位上等几个小时之后才发现基础配置错了。我个人在实际操作中体会最深的一点是JasperGold验证乘法模块这件事本质上是在做“数学等价性证明”而不是“靠运气找bug”。RTL写得越规整、时钟复位和流水线结构越清晰JasperGold发挥得越好。如果你拿到一个混乱的乘法模块寄存器乱命名、复位策略不统一、组合逻辑和时序逻辑混在一起形式验证的难度会指数级上升。所以从设计源头保证代码风格规整比事后在验证工具上花功夫要省力得多。本文还有配套的精品资源点击获取