简介本资源面向数字IC验证工程师与相关专业学习者聚焦基于Booth算法的乘法器模块在JasperGold环境下的形式化验证流程帮助读者掌握从黄金参考模型搭建到断言配置的完整验证思路。压缩包共7个文件约9KB包含TCL验证脚本、C语言黄金参考模型、Verilog RTL源码及Markdown说明文档等分别对应验证流程控制、参考行为建模、待验设计与使用指引。资源围绕握手、时钟、复位及数据输入输出信号展开涉及模块分析、时钟复位设置、断言添加、virtual_net逻辑简化与proof_structure验证步骤控制等关键环节并提及分支断言处理与验证空间优化等技术细节。目前已有133人学习适合希望借助实际源码理解JasperGold验证方法、快速上手乘法器形式化验证的读者参考。1. 乘法模块为什么成了形式验证的试金石一个 16×16 的定点乘法器RTL 代码不到 200 行仿真跑 10 万组随机激励也就几秒钟看起来完全没必要上形式验证。但真正做过乘法模块验证的人都知道随机仿真对乘法器的覆盖率增长曲线有多难看——前 80% 的覆盖率可能半天就跑到了剩下 20% 里的进位链边界、符号扩展组合、部分积压缩的极端情况跑一周随机激励也未必能碰到。这就是 JasperGold 这类形式验证工具真正值钱的场景它不靠碰运气而是用数学方法穷举状态空间要么证明属性在所有输入下成立要么给出一组反例波形。乘法模块之所以适合拿来做形式验证的入门练手对象是因为它规模适中、结构清晰、边界条件丰富。你不需要理解太复杂的设计意图就能写出有意义的断言同时它又足够“滑”稍不注意就会踩到溢出、位宽不匹配、有符号无符号混用这些经典坑。把乘法模块的 JasperGold 验证流程走通一遍基本上就掌握了形式验证的核心工作流写断言、设约束、跑证明、看反例、调策略。这篇内容面向的是已经写过 RTL、但还没系统用过 JasperGold 的验证工程师或者想从仿真验证往形式验证转的从业者。我会用一个无符号 16×16 乘法器作为被测对象从属性描述语言SVA写起一步步走到 JasperGold 的工程配置和证明策略调优。代码可以直接抄参数可以照着改坑我替你踩过了。2. 从 RTL 到 SVA乘法器属性怎么写才不漏2.1 先明确被测设计的接口和位宽约定在写任何断言之前必须先把被测模块的接口行为定义清楚。我一般会先画一张表把每个端口的位宽、有效周期、复位行为列出来避免后面写断言时位宽对不上。端口名方向位宽说明clkinput1时钟上升沿有效rst_ninput1异步复位低有效ainput16被乘数无符号binput16乘数无符号valid_ininput1输入有效标志youtput32乘积结果valid_outoutput1输出有效标志这里有一个容易忽略的点乘法器的延迟。组合逻辑乘法器当拍出结果流水线乘法器可能 2 到 4 拍出结果。断言里必须体现这个延迟关系否则 valid_out 和 y 的时序对不上形式验证会报出大量假反例。假设我们的被测设计是一个 2 级流水线乘法器输入有效后第 2 拍输出有效。这个假设必须和 RTL 实际行为一致不能凭感觉写。2.2 用 SVA 描述乘法器的核心属性乘法器最核心的属性就一条输出等于输入的乘积。但在流水线结构下这条属性需要加上时序延迟。下面是我常用的断言写法// 乘法器核心属性断言 // 假设流水线延迟为2拍valid_in拉高后第2拍valid_out拉高 property p_mul_correct; (posedge clk) disable iff (!rst_n) (valid_in) |- ##2 (valid_out (y a * b)); endproperty // 输出有效标志不能无故拉高 property p_valid_out_no_spurious; (posedge clk) disable iff (!rst_n) (!valid_out) |- ##1 (!valid_out || valid_in); endproperty // 复位后输出必须为零 property p_reset_output; (posedge clk) (!rst_n) |- ##1 (y 0 valid_out 0); endproperty a_mul_correct: assert property(p_mul_correct); a_valid_out_no_spurious: assert property(p_valid_out_no_spurious); a_reset_output: assert property(p_reset_output);这段代码的逻辑说明p_mul_correct是主属性用|-蕴含操作符表示当 valid_in 为真时经过 2 个时钟周期后 valid_out 必须为真且 y 等于 a*b。disable iff (!rst_n)表示复位期间不检查这条属性这是标准做法避免复位阶段产生无意义的反例。参数说明##2中的数字必须和 RTL 流水线级数严格一致。如果你不确定延迟是几拍可以先写一个宽松的断言比如##[1:4]跑一次形式验证看工具报出的反例波形确认实际延迟后再收紧。我见过太多人直接抄别人的##2结果自己的设计是 3 级流水线白白浪费半天排查时间。p_valid_out_no_spurious是一条辅助属性用来约束输出有效标志的行为。没有这条属性工具可能会找到一个 valid_out 在无输入时拉高的反例虽然主属性可能仍然成立但设计行为已经不对了。2.3 约束怎么写才不会把属性约束死形式验证和仿真的一个本质区别是仿真里你不给激励电路就不动形式验证里工具会自动探索所有可能的输入组合。所以你必须用约束constraint告诉工具哪些输入场景是不需要验证的否则状态空间会爆炸。// 输入约束valid_in不能连续超过4拍拉高 // 模拟实际场景中的背压行为 property p_valid_in_burst_limit; (posedge clk) disable iff (!rst_n) valid_in |- ##[1:4] !valid_in; endproperty // 约束写法用assume而不是assert c_valid_in_burst: assume property(p_valid_in_burst_limit); // 复位后至少保持4拍低电平 c_reset_hold: assume property( (posedge clk) (!rst_n) |- ##[1:4] (!rst_n) );这里的关键区别是assume和assert。assert是检查设计是否满足属性assume是告诉工具“我只关心满足这个条件的输入场景”。如果你把输入约束写成 assert工具会试图证明这个约束在所有情况下成立但输入是环境给的设计本身无法控制所以必须用 assume。参数说明##[1:4]表示 1 到 4 个时钟周期内的任意时刻。这个范围不能设得太宽否则工具探索的空间太大证明时间会急剧增加也不能设得太窄否则可能把合法的输入场景排除掉导致验证不完整。我一般会先设一个较宽的范围跑一次看看工具能不能在合理时间内收敛再逐步收紧。注意assume 约束是形式验证里最容易翻车的地方。约束太松状态空间爆炸工具跑不完约束太紧把 bug 场景排除了验证结果不可信。建议每加一条 assume都问自己一句这条约束在真实使用场景下一定成立吗3. JasperGold 工程配置与证明策略调优3.1 工程目录结构和最小配置文件JasperGold 的工程配置不像仿真工具那么直观很多人第一次用的时候会被一堆 tcl 命令搞晕。我一般会按下面的结构组织工程目录mul_fv/ ├── rtl/ │ └── mul_16x16.v ├── sva/ │ └── mul_assertions.sv ├── scripts/ │ └── run_fv.tcl └── jgproject/ └── (工具自动生成)最小化的 tcl 脚本如下# run_fv.tcl - JasperGold 乘法器验证脚本 # 清空之前的状态 clear -all # 读入RTL设计 analyze -sv rtl/mul_16x16.v # 读入SVA断言文件 analyze -sv sva/mul_assertions.sv # 展开设计层次指定顶层模块 elaborate -top mul_16x16 # 设置时钟和复位 clock clk reset -expression {!rst_n} # 设置证明策略先跑一遍基础证明 prove -all # 查看结果 report -summary这段脚本的逻辑说明analyze负责读入源文件并做语法检查elaborate负责展开设计层次并建立内部表示。clock和reset是必须设置的否则工具不知道时序关系。prove -all会尝试证明所有断言但第一次跑通常不会全部通过。参数说明-top后面跟的必须是 RTL 文件里定义的顶层模块名大小写敏感。reset -expression里的表达式要用花括号包起来这是 tcl 语法要求。如果你的复位是高有效改成{rst}即可。3.2 证明策略怎么从跑不完到跑得完JasperGold 默认的证明策略是“先易后难”但乘法器的状态空间很大默认策略经常跑几个小时也出不来结果。我一般会按下面的顺序调策略第一步先用prove -property单独证明每一条断言看看哪条最难。通常p_mul_correct是最难的因为它涉及完整的乘法运算。第二步对难证明的属性尝试增加抽象层次。比如把 16 位乘法拆成高 8 位和低 8 位分别证明或者用abstract命令把部分逻辑替换成黑盒。第三步调整证明引擎。JasperGold 支持多种证明引擎乘法器一般用-engine B效果比较好但这不是绝对的需要根据实际设计试。# 分步证明策略 # 先证明辅助属性建立不变量 prove -property {a_valid_out_no_spurious a_reset_output} # 对主属性使用更强的引擎和更长的超时 prove -property {a_mul_correct} -engine B -timeout 3600 # 如果还跑不完尝试用抽象 abstract -module mul_16x16 -instance u_mul -keep_ports prove -property {a_mul_correct} -timeout 1800参数说明-timeout的单位是秒3600 表示 1 小时。实际项目中我一般会设 1800 到 7200 之间太短了没意义太长了浪费机器时间。-engine B是 JasperGold 的一种证明引擎对算术运算类设计通常比默认引擎快但具体效果取决于设计结构。注意抽象命令abstract会改变设计的内部表示可能引入不精确性。如果抽象后属性通过了最好再用原始设计跑一次确认避免抽象掩盖了真实 bug。3.3 看反例波形怎么区分真 bug 和假反例形式验证报出反例counterexample的时候第一件事不是改 RTL而是判断这个反例是真的还是假的。假反例通常来自约束不完整或时序假设错误。我一般会按下面的清单排查排查项检查方法常见问题复位时序看反例波形里 rst_n 的跳变时刻复位释放和 valid_in 的时序关系没约束流水线延迟数 valid_in 到 valid_out 的拍数断言里的 ##N 和 RTL 不一致位宽扩展看 a*b 的位宽是否被截断16×16 的结果是 32 位但 y 只有 16 位有符号处理检查 a 和 b 是否被当成有符号数RTL 里用了 signed 但断言里没体现如果反例波形里 valid_in 在复位还没释放的时候就拉高了那基本可以确定是约束没写全不是设计 bug。如果反例波形里 valid_in 和 valid_out 的时序关系看起来正常但 y 的值确实不等于 a*b那就是真 bug需要回去查 RTL。我自己的习惯是每次看到反例先花 5 分钟确认波形里的时序关系再花 5 分钟手动算一下 a*b 的值最后才决定是改约束还是改 RTL。这个习惯帮我省了很多来回折腾的时间。4. 乘法器形式验证的五个血泪坑4.1 坑一位宽不匹配导致断言永远失败现象p_mul_correct一直报反例波形里 y 的值看起来“差不多对”但就是差一点。原因16 位乘 16 位的结果是 32 位但如果 RTL 里 y 只声明了 16 位高位会被截断。断言里y a * b比较的是 32 位结果和 16 位结果自然不相等。解决先确认 RTL 里 y 的位宽。如果是 32 位检查断言里的比较是否做了位宽扩展。如果是 16 位那断言应该写成y (a * b) 16hFFFF或者y a * b[15:0]具体取决于设计意图。4.2 坑二assume 约束把 bug 场景排除了现象所有断言都通过了但后来仿真里发现了一个明显的乘法错误。原因assume 约束写得太紧把出错的输入组合排除了。比如约束了a 0 b 0但设计在 a0 或 b0 时其实有 bug。解决每加一条 assume都要在仿真环境里跑一遍对应的随机激励确认这条约束在真实场景下确实成立。如果仿真里能出现违反约束的场景那这条 assume 就不能加。4.3 坑三复位释放和 valid_in 的时序竞争现象反例波形里 rst_n 刚拉高valid_in 就当拍拉高valid_out 在 2 拍后没有正确响应。原因断言里没有约束复位释放后 valid_in 的最小等待时间。真实电路里复位释放后通常需要几个周期稳定但形式验证工具不知道这个假设。解决加一条 assume 约束复位释放后至少 2 拍内 valid_in 不能拉高。具体拍数取决于你的设计一般 2 到 4 拍比较合理。4.4 坑四证明时间太长以为工具卡死了现象prove -all跑了 3 个小时还没出结果CPU 占用率 100%但没有任何输出。原因乘法器的状态空间是 2^32默认证明策略可能陷入穷举。这不是工具卡死是真的在算。解决先用prove -property单独证明简单的属性确认工具本身工作正常。然后对难证明的属性加-timeout限制超时后看工具给出的部分结果。如果确实跑不完考虑用抽象或分治策略。4.5 坑五SVA 里的 ##N 和 RTL 流水线级数不一致现象断言偶尔通过偶尔失败反例波形里 valid_out 的时序看起来“飘忽不定”。原因RTL 的流水线级数可能不是固定的比如在某些输入下走快速路径某些输入下走慢速路径。断言里写死了##2但实际延迟可能是 1 到 3 拍。解决先仔细阅读 RTL确认流水线结构是否固定。如果不固定断言里要用##[1:3]这样的范围并在属性里加上对 valid_out 的额外约束。如果固定那就把##N改成实际级数。5. 让证明收敛更快的一个实用技巧前面几章把基本流程走通了但实际项目中你很快会发现一个问题乘法器的形式验证跑一次要几十分钟甚至几个小时迭代效率太低。这一章分享一个我常用的技巧——用“分治证明”把大乘法器拆成小模块分别验证。核心思路很简单16×16 乘法器可以拆成 4 个 8×8 乘法器加上移位和加法。如果你能分别证明 4 个 8×8 乘法器是正确的再加上移位和加法的正确性就能推导出整个 16×16 乘法器正确。JasperGold 支持这种分治证明流程关键是写好“假设-保证”契约。具体做法是先为 8×8 子模块写一套断言证明它的输出等于输入乘积。然后在 16×16 顶层模块里用assume声明“8×8 子模块的输出是正确的”再用assert证明顶层输出正确。这样工具在证明顶层时不需要展开子模块的内部逻辑状态空间从 2^32 降到 2^16 级别证明时间通常能缩短一个数量级。// 8x8子模块的断言 module mul_8x8_assertions( input logic clk, rst_n, input logic [7:0] a, b, input logic valid_in, output logic [15:0] y, output logic valid_out ); property p_8x8_correct; (posedge clk) disable iff (!rst_n) valid_in |- ##1 (valid_out y a * b); endproperty a_8x8_correct: assert property(p_8x8_correct); endmodule // 16x16顶层里的假设 // 声明8x8子模块的输出是正确的 assume property( (posedge clk) disable iff (!rst_n) u_mul_8x8.valid_out |- (u_mul_8x8.y u_mul_8x8.a * u_mul_8x8.b) );这段代码的关键在于assume里的路径引用u_mul_8x8.valid_out直接指向子模块实例的内部信号。JasperGold 支持这种跨层次引用但需要确保子模块实例名和信号名完全正确。参数说明分治证明的粒度需要根据实际情况调整。8×8 拆成 4×4 可能过度拆分导致契约数量太多管理成本上升。我一般会先试 8×8 粒度如果证明时间还是太长再考虑拆到 4×4。这个技巧的代价是你需要额外维护子模块的断言和顶层假设之间的一致性。如果子模块断言改了但顶层假设没改可能会出现“子模块证明通过但顶层证明失败”的情况。我的习惯是每次改子模块断言都同步检查顶层假设确保两边说的是同一件事。还有一个细节分治证明对组合逻辑乘法器效果最好对流水线乘法器需要额外处理流水线寄存器的时序关系。如果你的乘法器是流水线结构建议先把流水线寄存器抽出来单独验证再验证组合逻辑部分。最后说一个我自己的教训刚开始用 JasperGold 的时候我总想一次跑通所有属性结果每次都要等几个小时。后来改成先跑辅助属性、再跑主属性、最后跑分治证明迭代速度至少快了 3 倍。形式验证不是跑一次就完事的它是一个反复调整约束和策略的过程。把迭代速度提上来比一次跑通更重要。希望帮到你。本文还有配套的精品资源点击获取