简介：本资源面向数字IC验证工程师与硬件设计学习者，聚焦基于Booth算法的乘法器模块在JasperGold环境下的形式化验证流程。包内共7个文件，以Verilog源码、TCL验证脚本、C语言黄金参考模型及Markdown说明文档为主，另含gitignore与inscode配置，压缩包约9KB，体量轻便便于快速上手。内容覆盖乘法器输入输出信号定义、握手与时钟复位处理、C模型宏定义与条件分支、TCL脚本中的模块分析、断言添加与验证辅助逻辑配置，并涉及virtual_net简化RTL逻辑、proof_structure控制验证步骤等进阶技巧，同时给出分支断言处理与验证空间优化的排错思路。已有133人学习，适合希望掌握JasperGold形式化验证方法、理解Booth乘法器验证细节的读者参考借鉴。
1. 乘法模块的形式验证为什么值得单独开一局
写 RTL 的人大多有过这种经历：仿真跑了几十万个激励，覆盖率报表也刷到了九十几，乘法器还是会在某个 corner case 上翻车——比如操作数刚好是0x8000_0000乘0x8000_0000，或者有符号数边界溢出。这类 bug 用随机仿真去撞，概率低到让人怀疑人生。JasperGold 验证乘法模块，本质上是把「穷举证明」这件事交给形式化引擎：给定一组输入位宽和约束，工具会尝试数学上证明输出恒等于参考模型，或者反过来给出一个反例波形。它适合谁？适合已经能写基本 SVA、手头有 RTL 源码、但被仿真覆盖率折磨过的验证工程师和设计工程师。源码在手，意味着你可以直接对模块端口做黑盒或白盒证明，不需要搭 UVM 环境，也不需要写 testbench 的 driver 和 monitor。这一章先把「为什么乘法模块特别适合形式验证」讲清楚，后面再落到具体命令和参数。
乘法器的特殊性在于它的功能完全由输入输出关系定义，没有状态机、没有握手协议、没有跨时钟域，所有行为都收敛在一个组合逻辑或者单周期时序逻辑里。这种「纯函数」式的模块，恰恰是形式化工具最擅长的对象。你不需要构造复杂的场景序列，只需要把输入空间约束好，让工具去证明product == a * b这个断言。相比之下，一个带缓存的 DMA 控制器做形式验证，光是把环境约束写对就要花掉大半时间。乘法模块的验证周期通常以小时计，而不是以天计。另一个现实原因是，乘法器在 DSP、AI 加速器、加密协处理器里都是关键路径，一旦出错就是系统性错误，流片后无法用软件补丁绕过。所以花半天时间做一次完整证明，投入产出比非常高。
2. 从 RTL 到 JasperGold：环境搭建与参考模型选择
2.1 目录结构与最小文件集
我一般会把形式验证的工程目录和 RTL 目录分开，避免工具生成的中间文件污染源码树。一个最小可跑的目录长这样：
mul_fv/ ├── rtl/ │ └── mul.v ├── fv/ │ ├── mul_fv.tcl │ └── mul_ref.sv └── run/rtl/mul.v是待验证的乘法模块源码，fv/mul_ref.sv放参考模型和断言，fv/mul_fv.tcl是 JasperGold 的批处理脚本。run/目录用来执行，所有 log 和数据库都落在这里，删起来方便。不要小看这个习惯，我见过有人把工具数据库和 RTL 混在一起，最后git status里全是二进制文件，清理起来非常痛苦。
2.2 参考模型：行为级乘法还是查找表
参考模型的选择直接决定证明的难度和可信度。常见做法有三种：
第一种是直接用 Verilog 的*运算符写一个行为级乘法。这是最省事的，但有个隐患：如果综合工具或者形式工具对*的处理和你的 RTL 实现有细微差异，证明可能会失败，而你分不清是 RTL 错了还是参考模型错了。第二种是用移位加法循环写一个周期级的参考模型，逐位累加。这种模型和 RTL 结构接近，证明容易过，但参考模型本身也可能有 bug，相当于用可能有问题的东西去证明另一个东西。第三种是查表法，只适用于小位宽，比如 4 位乘 4 位，直接把 256 种结果写成 case 语句。这种方式最可信，但位宽一大就不现实。
我的建议是：对于 8 位以内的乘法，用查表或者 Python 生成的真值表；对于 16 位以上，用行为级*加上独立的边界断言。下面是一个 8 位无符号乘法的参考模型片段：
// mul_ref.sv module mul_ref ( input logic [7:0] a, input logic [7:0] b, output logic [15:0] product ); assign product = a * b; endmodule这个模块本身不参与综合，只作为形式验证的参考。JasperGold 会把它和 DUT 的输出做比较。
2.3 断言写法：三种等价性检查策略
断言是形式验证的核心。对于乘法模块，我通常会用三种策略组合：
第一种是直接等价性断言，比较 DUT 输出和参考模型输出：
// 在 bind 或者顶层中 assert property ( @(posedge clk) disable iff (!rst_n) (dut_product == ref_product) );第二种是代数性质断言，比如交换律a*b == b*a、零元a*0 == 0、单位元a*1 == a。这些断言不依赖参考模型，可以独立证明 RTL 的正确性。第三种是边界断言，针对有符号数的最小负数、无符号数的最大值等。
// 交换律 assert property ( @(posedge clk) disable iff (!rst_n) (dut_product(a, b) == dut_product(b, a)) ); // 零元 assert property ( @(posedge clk) disable iff (!rst_n) (dut_product(a, 8'h00) == 16'h0000) );这三种策略的关系是：等价性断言覆盖面最广，但依赖参考模型；代数断言独立性强，但覆盖不了所有输入组合；边界断言针对性强，但数量有限。三者叠加，才能既保证覆盖率又保证可信度。
2.4 Tcl 脚本：从 analyze 到 prove 的完整流程
JasperGold 的批处理流程一般分四步：analyze读入 RTL 和参考模型，elaborate展开层次，clock定义时钟和复位，prove启动证明。下面是一个可以直接抄的脚本：
# mul_fv.tcl # 清空之前的状态 clear -all # 读入 RTL 和参考模型 analyze -sv rtl/mul.v analyze -sv fv/mul_ref.sv # 展开顶层，指定 DUT 顶层模块 elaborate -top mul_top # 定义时钟和复位 clock clk reset ~rst_n # 设置证明属性 prove -all # 生成报告 report -summaryanalyze的参数-sv表示按 SystemVerilog 解析。如果你的 RTL 是纯 Verilog-2001，可以用-v或者-verilog。elaborate -top指定顶层模块名，这个模块必须包含 DUT 和参考模型的实例化。clock和reset告诉工具时序行为，如果是纯组合逻辑乘法器，可以省略这两行，但加上也不影响。prove -all会尝试证明所有断言，如果失败会给出反例。report -summary输出一个简表，包含每个断言的证明状态：proven、cex（反例）、undetermined。
2.5 参数怎么设：位宽、约束和引擎选择
位宽是第一个要确认的参数。DUT 的输入位宽必须和参考模型一致，否则等价性断言会直接失败。如果 DUT 是参数化模块，在elaborate时用-param覆盖：
elaborate -top mul_top -param WIDTH 16约束方面，如果乘法器有 valid 信号或者流水线使能，需要用assume约束输入空间。比如只验证 valid 为高时的行为：
assume property ( @(posedge clk) disable iff (!rst_n) (valid |-> !$isunknown(a) && !$isunknown(b)) );引擎选择上，JasperGold 默认会自动选。对于乘法器这种数据路径为主的模块，我一般会显式指定-engine为B或者I。B是 BDD 引擎，适合位宽小、逻辑深的模块；I是插值引擎，适合位宽大、结构规整的乘法器。如果证明跑不动，可以试试-engine C，这是基于 SAT 的引擎，对组合逻辑比较友好。具体命令：
prove -all -engine I -timeout 3600-timeout单位是秒，超过时间会返回 undetermined，而不是一直卡住。
3. 证明跑不动怎么办：分治、切分与抽象
3.1 为什么 32 位乘法器会让工具卡死
32 位乘法器的输入空间是 2 的 64 次方，任何形式工具都不可能暴力穷举。JasperGold 的引擎虽然聪明，但面对纯组合的 32 位乘法，BDD 会爆炸，SAT 会超时。这不是工具的问题，是问题本身的计算复杂度决定的。我见过有人试图直接 prove 一个 32 位乘法器，跑了三天三夜还是 undetermined，最后放弃。正确的做法是分治。
3.2 按位切分：把 32 位拆成 4 个 8 位
最常见的分治策略是按位切分。一个 32 位乘法可以拆成四个 8 位乘法的组合，每个 8 位乘法的输入空间只有 2 的 16 次方，工具几秒钟就能证完。具体做法是：在 RTL 中把乘法器实例化成四个子模块，每个子模块负责 8 位部分积，然后在顶层做移位相加。形式验证时，先证明每个子模块的正确性，再证明顶层加法树的正确性。这样每个证明的规模都控制在工具能处理的范围内。
// 子模块断言 module mul8_fv ( input logic [7:0] a, input logic [7:0] b, output logic [15:0] product ); assert property ( @(posedge clk) disable iff (!rst_n) (product == a * b) ); endmodule顶层加法树的证明可以用assume把子模块的输出当作自由变量，只验证移位和加法的正确性。这样就把一个不可解的问题拆成了五个可解的问题。
3.3 用 assume 约束输入空间：不是作弊，是聚焦
有人觉得用assume约束输入是「作弊」，其实不是。形式验证的目标是证明「在合法输入下，输出正确」，而不是证明「在所有可能的二进制组合下都正确」。如果乘法器的输入来自一个 AXI 接口，而 AXI 协议规定了某些位不会同时为高，那你完全可以把这些约束写进assume。关键是约束要来自设计规格，而不是为了证明通过而随意添加。
// 假设输入不会同时为 X assume property ( @(posedge clk) disable iff (!rst_n) (!$isunknown(a) && !$isunknown(b)) );$isunknown是 SystemVerilog 的系统函数，用来检查是否有 X 或 Z。加上这个约束后，工具不需要考虑未知态，证明空间会小很多。
3.4 抽象：用黑盒替换已知正确的子模块
如果乘法器内部调用了某个已经验证过的加法器或者 Booth 编码器，可以在形式验证时把这些子模块黑盒化，只保留接口。JasperGold 支持-blackbox选项：
elaborate -top mul_top -blackbox {booth_enc adder_tree}黑盒化之后，工具会把被黑盒的模块输出当作自由变量，不再展开内部逻辑。这能显著降低证明复杂度，前提是你确信这些子模块是正确的。如果子模块本身有问题，黑盒化会掩盖 bug，所以只对已经独立验证过的模块这么做。
4. 避坑与排查：乘法形式验证的五个血泪教训
4.1 现象：证明通过但流片后出错
原因：参考模型和 RTL 用了同一个有 bug 的*运算符，等价性断言变成了「自己证明自己」。解决：参考模型尽量用查表或者独立的算法实现，不要和 RTL 共享任何代码。如果 RTL 用 Booth 编码，参考模型就用移位加法，确保两者在实现上完全独立。
4.2 现象：工具报 cex，但波形看起来是对的
原因：时钟和复位定义不一致。比如 RTL 是低电平复位，但 Tcl 里写了reset rst_n，工具会按高电平复位处理，导致时序错位。解决：确认reset后面的信号名和极性。如果是低电平复位，写reset ~rst_n。另外检查clock定义的边沿是否和 RTL 一致，上升沿触发就写clock clk，下降沿要加-edge fall。
4.3 现象：undetermined 跑了很久不结束
原因：输入位宽太大，或者约束太少导致状态空间爆炸。解决：先检查是否有assume约束可以加，然后尝试分治。如果分治后还是 undetermined，换引擎试试。BDD 不行换 SAT，SAT 不行换插值。还可以用-timeout限制单次证明时间，避免无限等待。
4.4 现象：有符号乘法边界出错
原因：有符号数的符号扩展没有正确处理。比如 8 位有符号数-128乘-128，结果应该是16384，但 RTL 可能因为符号位扩展错误得到负数。解决：针对有符号数单独写边界断言，覆盖最小值、最大值、零、正负交替等组合。参考模型也要用signed关键字明确声明。
logic signed [7:0] a_signed, b_signed; logic signed [15:0] product_signed; assign product_signed = a_signed * b_signed;4.5 现象：证明结果不稳定，每次跑结论不一样
原因：工具使用了随机种子或者多线程调度，导致搜索顺序不同。解决：在 Tcl 里固定种子set_proofgrid_seed 12345，并关闭多线程set_proofgrid_max_jobs 1。虽然会慢一点，但结果可复现。另外，如果用了-timeout，超时边界附近的证明可能会时过时不过，建议把超时设大一些，或者把断言拆细。
5. 进阶技巧：用 cover 属性反查证明盲区
证明通过不代表覆盖完整。JasperGold 的cover属性可以告诉你哪些输入组合被证明过程实际访问过。如果某个 cover 一直不命中，说明你的约束可能过紧，或者证明引擎走了捷径。我一般会加一组 cover 来检查边界情况：
cover property ( @(posedge clk) disable iff (!rst_n) (a == 8'hFF && b == 8'hFF) ); cover property ( @(posedge clk) disable iff (!rst_n) (a == 8'h80 && b == 8'h80) );跑完prove之后，用report -cover查看命中情况。如果a == 8'hFF && b == 8'hFF没有命中，说明证明过程根本没有考虑这个组合，即使断言通过了也不能放心。这时候需要检查assume是否意外排除了这个组合，或者换一个引擎重新证明。
另一个技巧是用-proofgrid做分布式证明。JasperGold 支持把多个断言分发到不同机器上并行跑，适合断言数量多、单个断言规模不大的场景。命令是prove -all -proofgrid，具体配置在proofgrid.tcl里。我一般会在回归阶段用这个模式，把一晚上能跑完的证明压缩到两三个小时。
最后说一个我自己的习惯：每次证明通过后，我会故意把 RTL 里的某个+改成-，重新跑一遍，确认工具能报出 cex。如果改了错误还能证明通过，说明断言写得太弱，或者约束把错误路径屏蔽了。这个「反向测试」花不了几分钟，但能救命。希望帮到你。
本文还有配套的精品资源，点击获取
