简介面向数字IC验证场景的JasperGold乘法器验证源码包聚焦Booth算法乘法模块的形式化验证流程适合希望了解JasperGold断言验证与黄金参考模型构建的数字电路验证工程师或学习者。压缩包共7个文件以C黄金参考模型、TCL验证脚本、Verilog设计文件及Markdown说明文档为主整体仅9KB内容紧凑便于快速浏览和复用。内容涵盖C模型宏定义、输入输出条件分支以及TCL断言编写等关键知识点。已有131人学习包内内容虽少但覆盖完整验证路径从握手时钟/复位等信号梳理到C模型行为对齐、断言添加再到virtual_net简化RTL与proof_structure控制验证步骤均提供具体代码或脚本示例。从中可以梳理出一套用JasperGold验证Booth乘法器的可行方法也能了解分支断言处理、验证空间优化等细节对开展类似形式化验证工作有直接参考价值也可作为自建验证环境的起点。1. 把JasperGold验证乘法模块当成普通仿真任务第一天就会碰壁一个 12 位乘 12 位的乘法模块输入组合足足有 2^24 种仿真回归通常只能拿典型值、边界值和随机激励去撞撞不到的那部分恰好最容易藏问题截断位宽差一位、符号扩展写反、溢出标志在多周期流水里晚了一拍。JasperGold 验证乘法模块这件事的核心是把乘法器的 RTL 源码和 SVA 断言一起交给形式求解器让它数学式地遍历所有输入组合要么证明断言成立要么直接给出一条具体反例。对数据通路验证来说这比堆几千行 UVM 平台更直接。这篇笔记按我实际跑过的路径来写先从源码读出位宽和截断规则再写参考模型和断言最后用 JasperGold 的命令行脚本跑通并排掉那些一眼看不出来的假反例。2. JasperGold验证乘法模块前先拆清位宽、截断和符号形式验证为什么能一次跑完验证乘法模块最容易犯的错是把“乘出来对不对”当成唯一目标。实际上一个乘法器在真实总线里工作至少要回答三个问题全精度乘积是否计算正确输出位宽截断后是否符合设计约定有符号场景下符号扩展和溢出标志是否跟得上乘积。这三个问题各自对应不同的 RTL 缺陷仿真平台想覆盖全需要按位宽和符号组合写测试用例数量会膨胀得很难看。我从一个 12 位无符号乘法器说起。12 位乘 12 位的全精度结果是 24 位输入组合共 2^24也就是 16,777,216 种。动态仿真如果每种组合跑一拍加上流水延迟和结果比较等效时间并不算大但真实设计里通常还有使能信号、流水级、截断模式、复位时序组合起来就是一个几十维的状态空间穷举完全不可能。更麻烦的是乘法结果的错误往往集中在少数边界模式上例如 a 取最大值、b 取 0、结果恰好落在截断边界。靠随机激励碰到这些模式的概率很低而形式验证在处理这类“输入空间大、控制逻辑简单”的数据通路时正好有优势。2.1 乘法模块要验的不只是“乘出来对不对”三层目标和两个输出边界我给乘法模块列验证目标时通常会分成三层。第一层是全精度乘积正确性也就是在使能有效且无额外约束时输出等于两个输入数学相乘的结果。这一层解决的是乘法器本身做没做对的问题比如 Booth 编码选错、部分积压缩树接错、进位链断掉。第二层是输出位宽和截断行为说到底是确定最终输出到底保留乘积的高半部分还是低半部分以及是否有饱和、舍入逻辑。第三层是时序行为包括有效信号与数据对齐、多周期流水的延迟节拍、溢出标志拉高的时机。两个输出边界分别是最大值边界和符号边界。无符号乘法里输入全为最大值时乘积的最高位会被置起如果设计把最高位截掉但总线声明仍按原宽度扩展结果会差一个 2 的幂次。有符号乘法里负负得正时符号位翻转但高位扩展如果仍按某个输入的最高位做乘积就会在视觉上变成负数。动态仿真通常能覆盖到前一个边界后一个边界要看测试用例设计者的经验。JasperGold 验证乘法模块的一个明显好处是它把断言和设计源码编译成数学约束后求解器会主动去找违反断言的输入序列。它不会像仿真那样从第一条测试用例开始跑而是直接瞄准断言的否命题去构造反例。对上述三层目标只要断言写得对求解器就能把所有输入组合一起处理省去枚举激励的过程。2.2 为什么选JasperGold而不是多写几千行UVM平台形式验证的适用边界选 JasperGold 还是选动态仿真平台我一般看两个条件设计是否以数据通路为主以及断言能否从源码直接推导。乘法模块、加法树、FFT 蝶形单元这类设计非常符合因为它们几乎没有复杂的控制状态机没有外部存储交互输入输出关系用一个数学表达式就能描述。反过来如果乘法器嵌在一个带握手状态机、有多个优先级仲裁的总线接口里形式验证的难度会明显上升这时动态仿真平台更合适。JasperGold 与传统 UVM 平台的对比我习惯用一张表说清楚。对比项动态仿真平台UVMJasperGold 形式验证输入覆盖方式按测试用例逐条驱动求解器自动遍历合法输入空间反例输出需要自己比对结果反例停留在波形层直接给出使断言失败的输入序列和对应时刻对复杂协议的适配握手、乱序、总线协议模拟能力强协议约束越复杂求解难度越大数据通路数学逻辑适合但需要大量用例覆盖边界适合边界自动被搜索调试效率波形逐拍查比较耗时反例可回放配合报告能快速定位从这个表可以得出一个简单结论乘法模块这种纯数据通路形式验证的投入产出比明显高于写一套完整 UVM 平台但如果模块周围有复杂协议我不会只用 JasperGold而是把它跟仿真回归互补使用。形式验证也不是把源码读进去就可以直接开始。JasperGold 需要一个最小工程包含设计源码、断言源码、约束文件和运行脚本。我在下面列了这份文件清单后面章节会逐个展开。文件作用说明rtl/mul_unit.sv被测乘法模块 RTL需要明确位宽参数、输出截断方式assert/mul_assert.svSVA 断言与参考模型断言断言逻辑与 RTL 分离不改设计源码tb/mul_constraints.sv输入约束assume约束使能信号和数据稳定的关系scripts/run_jg.tclJasperGold 脚本负责读文件、设时钟复位、跑 prove实际工程里断言文件可以单独放也可以作为 bind 模块挂到设计上。我一般倾向单独编译再用 bind 方式加载这样 RTL 源码保持原样JasperGold 验证的完全就是即将交付的那个乘法模块不会因为验证代码混在设计中引入额外差异。3. 从乘法模块源码读到位参考模型、SVA断言与第一个跑通的JasperGold脚本在写任何断言之前先做一件看起来像在读源码、实际决定后面所有验证结果的事把乘法模块的输入位宽、输出位宽、截断规则、流水级数从源码里确认一遍。这一步不做好断言写出来往往不是逻辑错误而是和 RTL 的位宽定义根本不在一个坐标系里。3.1 先读源码从乘法模块代码里抽出位宽、截断与流水级一个基础的无符号乘法流水模块我通常会写成下面这样的形态它不复杂但已经包含位宽参数和流水寄存// rtl/mul_unit.sv module mul_unit #( parameter int W 12 ) ( input logic clk, input logic rst_n, input logic valid_i, input logic [W-1:0] a_i, input logic [W-1:0] b_i, output logic valid_o, output logic [2*W-1:0] product_o ); logic [2*W-1:0] product_r; logic valid_r; always_ff (posedge clk or negedge rst_n) begin if (!rst_n) begin product_r 0; valid_r 1b0; end else begin product_r {{W{1b0}}, a_i} * {{W{1b0}}, b_i}; valid_r valid_i; end end assign product_o product_r; assign valid_o valid_r; endmodule这里最值得注意的一行是{{W{1b0}}, a_i} * {{W{1b0}}, b_i}。我不直接写a_i * b_i因为 SystemVerilog 里乘法表达式的位宽由上下文决定赋值目标 product_r 是 2W 位所以这个乘法会在 2W 位上下文里计算。直接把两个 W 位数相乘如果没有位宽上下文结果只取 W 位乘积的高位会被悄悄丢掉。用{{W{1b0}}, a_i}把每个输入先零扩展成 2W 位再进入乘法可以保证全精度结果完整落在 product_r 中。参数 W 是输入位宽默认给 12。product_r 的位宽必须写成2*W这一步写错后面所有断言都会跟着错。valid_r 把 valid_i 打一拍让有效标志与乘积结果对齐这是流水验证的基准点。读出这些信息后才能确定断言里参考模型的位宽和时序。3.2 参考模型加断言验证源码里最容易写错的一行读完成源码下一步是写验证源码。验证乘法模块的断言核心不是直接写“product_o 等于 a 乘 b”而是先写一个独立的参考模型让参考模型把输入打拍和乘积计算都做一遍再断言设计输出与参考模型输出一致。直接比较的最大问题在于SVA 断言表达式里没有赋值目标两个 W 位输入相乘时乘积位宽按最大操作数位宽取结果会截断到 W 位跟 2W 位的 product_o 比较时必然出现大量假反例。一个能直接用的断言模块是这样的// assert/mul_assert.sv module mul_assert #( parameter int W 12 ) ( input logic clk, input logic rst_n, input logic valid_i, input logic [W-1:0] a_i, input logic [W-1:0] b_i, input logic valid_o, input logic [2*W-1:0] product_o ); logic [2*W-1:0] ref_product_r; logic ref_valid_r; always_ff (posedge clk or negedge rst_n) begin if (!rst_n) begin ref_product_r 0; ref_valid_r 1b0; end else begin ref_product_r {{W{1b0}}, a_i} * {{W{1b0}}, b_i}; ref_valid_r valid_i; end end property p_product_ref; (posedge clk) disable iff (!rst_n) ref_valid_r |- (product_o ref_product_r); endproperty assert property (p_product_ref); endmodule这个断言模块我建议通过 bind 挂到设计上不改动 mul_unit 的源码。参考模型 ref_product_r 和设计内部 product_r 的赋值方式完全一致都先把输入零扩展到 2W 位再乘。ref_valid_r |- (product_o ref_product_r)的意思是当参考模型的有效标志为高时设计输出的乘积必须与参考模型一致。这里要特别说明一下断言里ref_valid_r的作用。它把 valid_i 打了一拍让有效标志和数据处在同一拍。|-在 SVA 里表示前件成立的下一拍检查后件采样时取的是寄存器更新前的值所以 ref_valid_r 为高的那一拍product_o 和 ref_product_r 都还保持着刚才同一组输入算出的结果比较才是有效的。如果不用 ref_valid_r 而直接拿 valid_i 做前件乘积还没有打拍完成比较会在错误的时间点发生。3.3 跑通最小JasperGold脚本read_file、clock/reset、prove三步源码和断言准备好后就需要 JasperGold 的命令行脚本了。我一般在工程目录下放一个 run_jg.tcl用 jg 的批处理模式直接跑内容和下面这个最小脚本是同一套思路# scripts/run_jg.tcl # 第一步读入设计和断言源码 read_file -format sverilog {rtl/mul_unit.sv assert/mul_assert.sv} # 第二步elaborate 顶层设计 elaborate -top mul_unit # 第三步声明时钟与复位 clock -port clk reset -port rst_n -value 0 # 第四步跑属性证明设置超时时间 prove -property {p_product_ref} -timeout 300第一步 read_file 会把设计源码和断言源码一起读进 JasperGold这里顺序没有严格要求但我习惯把设计放前面、断言放后面这样 elaborate 时顶层关系更清楚。第二步 elaborate 是必须的JasperGold 只有完成 elabora 后才知道 mul_unit 里有几个实例、哪些信号是端口。第三步 clock 和 reset 声明是整个脚本最容易漏的部分如果不告诉工具 clk 是时钟、rst_n 是低有效复位形式引擎会把这些端口当成普通自由输入prove 结果毫无意义。第四步 prove 里-timeout 300表示单条属性最多跑 300 秒超时后工具会返回 undetermined 状态不会一直空转。启动方式并不复杂通常执行一个jg命令后跟脚本路径即可也可以用调试模式让非批处理方式打开界面。这里不展开图形界面操作因为验证乘法模块这种数据通路脚本比界面更适合回归和版本管理。prove 返回的结果就三种proved 表示断言在给定约束下成立cex 表示找到了反例undetermined 表示超时或求解器没有得出结论。第一次跑通时如果结果是 proved还不能放松先要确认它是在正确的 clock/reset 设置下跑出来的然后再看反例报告。我通常会在 prove 之后执行一次 report 命令把断言状态和覆盖情况统一打出来再决定下一步是收敛还是要继续调约束。4. 截断、有符号乘法和多周期流水验证乘法模块的3个必调参数全精度乘积验证通过只是第一步真实总线上的乘法模块几乎都会做输出截断有符号设计还要处理符号扩展和溢出标志流水线深度不同也会直接影响断言写法。这几个点不是可选项而是验证乘法模块的必调参数。4.1 截断模式的断言保留低半和保留高半的参考模型怎么分我们先看一个常见的硬件设计输入是 W 位程序只保留乘积的低 W 位也就是取模结果。这种截断模式在 DSP 累加器和哈希计算里非常常见RTL 往往写成下面这样// rtl/mul_trunc_low.sv module mul_trunc_low #( parameter int W 12 ) ( input logic clk, input logic rst_n, input logic valid_i, input logic [W-1:0] a_i, input logic [W-1:0] b_i, output logic [W-1:0] product_o ); logic [2*W-1:0] product_r; logic valid_r; always_ff (posedge clk or negedge rst_n) begin if (!rst_n) begin product_r 0; valid_r 1b0; end else begin product_r {{W{1b0}}, a_i} * {{W{1b0}}, b_i}; valid_r valid_i; end end assign product_o product_r[W-1:0]; endmodule这里的输出 product_o 只取 product_r 的低 W 位验证断言就不能再拿全精度参考模型去比。参考模型在打完拍后需要额外截取一次低位// assert/mul_assert_trunc.sv logic [W-1:0] ref_product_trunc; always_ff (posedge clk or negedge rst_n) begin if (!rst_n) begin ref_product_trunc 0; end else begin ref_product_trunc {{W{1b0}}, a_i} * {{W{1b0}}, b_i}; end end property p_trunc_low; (posedge clk) disable iff (!rst_n) ref_valid_r |- (product_o ref_product_trunc[W-1:0]); endproperty注意一个细节ref_product_trunc 是 W 位寄存器不能直接拿它跟 product_o 比因为在赋值时它已经只保留了低 W 位如果 W 位寄存器跟 W 位输出比较看似没问题但一旦设计实现里截断的是高 W 位这个断言不会立刻抓住错误因为参考模型也已经同步截错了。最稳妥的做法是先保存全精度乘积再在比较时刻显式写ref_product_trunc[W-1:0]或[2*W-1:W]把截断方式摆在明面上。保留高半部分的截断参考模型写成product_o ref_product_r[2*W-1:W]但要注意高位保留通常伴随饱和或舍入逻辑这时直接位截取断言会失败。解决方法是跟设计规格逐条对照把舍入条件先单独验证再验证截断结果。4.2 有符号乘法和溢出标志符号扩展的两种错误写法有符号乘法验证里符号扩展是最大的坑。我见过至少两种错误写法一种是在输入上直接套$signed(a_i) * $signed(b_i)却不扩展位宽另一种是把符号位扩展到一半就参加乘法运算。两种都会导致负边界时乘积结果与手算差一个符号位。有符号参考模型的标准做法是先把输入符号扩展到 2W 位再做乘法乘积全精度保存// assert/mul_assert_signed.sv logic [2*W-1:0] ref_product_s; always_ff (posedge clk or negedge rst_n) begin if (!rst_n) begin ref_product_s 0; end else begin ref_product_s $signed({ {W{a_i[W-1]}}, a_i}) * $signed({ {W{b_i[W-1]}}, b_i}); end end{ {W{a_i[W-1]}}, a_i}把 a_i 符号位重复 W 次后拼在 a_i 前面得到 2W 位有符号数再做乘法。这样即使 W 位输入本身没有显式声明为 signed符号扩展规则也完全取决于最高位而不是取决于信号声明。比较时ref_product_s 和 design 的 product_o 都以位模式比较不要混用 signed 和 unsigned 的类型声明否则 SystemVerilog 的二元运算扩展规则会在某些组合下把两个操作数都按无符号处理制造出假反例。溢出标志的验证属于“第三层目标”。假设设计输出保留低 W 位额外拉出一个溢出标志 overflow_o正确溢出判断是全精度乘积的高 W 位不等于符号位的扩展。写成断言就是property p_overflow_flag; (posedge clk) disable iff (!rst_n) ref_valid_r (ref_product_s[2*W-1:W] ! {W{ref_product_s[W-1]}}) |- overflow_o; endproperty这条断言的意思是当全精度乘积的高半部分不是低半部分符号位的重复时说明结果已经超出 W 位有符号表示范围overflow_o 必须在这一拍拉高。反向断言同样要写即未溢出时 overflow_o 必须为低两个方向都 proved溢出标志才算验证完成。4.3 多周期乘法属性延迟和参考打拍如何对齐很多乘法模块不是单拍出结果而是流水线分成两级或三级。JasperGold 验证这类设计时最容易翻车的是参考模型打拍的节奏和设计不一致。三级流水乘法器里valid_i 在第 0 拍有效product_o 在第 3 拍才稳定断言如果按单拍写必定报反例。常见做法是把断言里的对齐关系写成参数化延迟// assert/mul_assert_pipe.sv parameter int D 3; // 流水深度 property p_pipeline_mul; (posedge clk) disable iff (!rst_n) valid_i |- ##D (valid_o product_o ref_product_r); endproperty这里的 D 是流水深度。ref_product_r 仍然按照单拍的方式在 valid_i 有效时采集输入并计算乘积但它本身不会延迟 D 拍所以上面的属性比对的是第 D 拍时的 ref_product_r 与 product_o。需要注意ref_product_r 在第 D 拍时可能已经被后续新的 valid_i 刷新因此更严谨的做法是把参考乘积同样打 D 拍让二者在时间上完全对齐logic [2*W-1:0] ref_product_pipe [D-1:0]; always_ff (posedge clk or negedge rst_n) begin if (!rst_n) begin for (int i 0; i D; i) ref_product_pipe[i] 0; end else begin ref_product_pipe[0] {{W{1b0}}, a_i} * {{W{1b0}}, b_i}; for (int i 1; i D; i) ref_product_pipe[i] ref_product_pipe[i-1]; end end然后断言直接比较ref_product_pipe[D-1]和product_o。这样参考模型和设计在每一级都有对应关系即使中间插入 valid_o 的对齐逻辑也能清楚看到是在哪一级错位。JasperGold 在跑多周期反例时报告会给出一个时序窗口通常是从 valid_i 拉高到 product_o 稳定之间的那几拍对照参考模型的各级值能很快定位是流水寄存器断连还是有效标志提前拉高。5. JasperGold验证乘法模块的5个典型坑现象、原因和排查步骤形式验证的好处是反例给得精确但反例本身也可能是在误导你。乘法模块里有一批问题现象是 prove 报出一堆 cex真正原因却是断言或环境设置不对而不是 RTL 错误。下面五条是我实际排查中遇到过的典型情况。5.1 假反例断言里直接写“a*b”导致位数被截断现象prove 在几秒内返回反例反例里 a 和 b 都不是边界值手工算一下乘积和 product_o 完全对得上但断言还是报错。原因断言表达式里直接写了product_o a_i * b_i而 SVA 表达式没有赋值目标乘法结果位宽按操作数最大位宽取两个 W 位输入相乘只保留 W 位与 2W 位的 product_o 比较时高位补零后必然不等。解决不要在断言里直接写乘法表达式先通过参考模型给乘法提供完整的 2W 位赋值上下文再比较寄存器值。5.2 有符号负边界反例成堆符号扩展写错差一个符号位现象无符号乘法断言全绿切到有符号后负边界输入如 a-1、b1 时反例成堆且每个反例的差异都集中在最高位附近。原因$signed(a_i)只改变操作数的解释方式不改变位宽两个 W 位有符号数相乘时乘积仍按 W 位结果处理缺少符号扩展。解决参考模型里用{ {W{a_i[W-1]}}, a_i}先做符号扩展再进入乘法比较时按位模式比较避免 signed/unsigned 类型混用。5.3$past在多周期乘法上失灵动态仿真过、形式验证翻车现象同一套断言在动态仿真里通过了拿到 JasperGold 里跑多周期流水场景立刻报反例反例的时间窗口和手算结果对不上。原因$past(expr, 1)只回溯一拍三级流水需要回溯三拍而且形式引擎处理$past嵌套时容易产生额外的约束复杂度。解决放弃$past把参考乘积按流水深度打 D 拍属性延迟写成##D让参考模型和设计按同一节拍对齐。5.4 反例时序不可能出现忘记给输入写assume约束现象反例显示 valid_i 为低时 product_o 发生了跳变或者 a_i、b_i 在 valid_i 为高时同时变化而实际总线协议根本不允许这种输入。原因JasperGold 认为所有输入都是自由信号没有给输入协议加 assume形式引擎就会尝试各种在真实系统中不存在的输入序列。解决给输入加约束例如assume property ((posedge clk) valid_i |- $stable(a_i) $stable(b_i));把数据在有效时的稳定性声明为假设反例就会收敛到合理输入空间内。5.5 断言一直证明不完或秒回无效反例clock/reset没设干净现象prove 跑到超时仍未下结论或者秒回一个反例反例里 rst_n 和 clk 的值看起来很奇怪像是被当成普通逻辑信号处理。原因脚本里漏了 clock 和 reset 声明JasperGold 把时钟端口当自由输入导致所有时序逻辑的推进方式都不可预测。解决在 elaborate 之后显式执行 clock 和 reset 两条命令并在断言里写清disable iff (!rst_n)低有效复位要确认复位值和复位有效电平一致。跑批处理脚本时先单独跑一条最简单的断言验证环境干净再放开到全部属性。6. 验证收敛用cover和报告确认断言不是自嗨prove 返回 proved 不等于验证工作结束。一个断言可能在给定约束下成立但约束本身可能过强把真正会触发的错误模式屏蔽掉了也可能断言本身覆盖的只是全精度路径截断路径和边界组合根本没被求解器认真探索过。我的做法是在 prove 之外再补 cover 和覆盖率报告把验证收敛的最后一环补上。cover 的写法跟断言类似区别在于它不需要检查结果只要求某个条件被触发过。对乘法模块来说我通常会加下面几条覆盖属性// assert/mul_cover.sv property cover_max_mul; (posedge clk) disable iff (!rst_n) valid_i (a_i {W{1b1}}) (b_i {W{1b1}}); endproperty property cover_zero_mul; (posedge clk) disable iff (!rst_n) valid_i (a_i 0) (b_i {W{1b1}}); endproperty property cover_neg_boundary; (posedge clk) disable iff (!rst_n) valid_i (a_i[W-1]) !(b_i[W-1]); endproperty cover property (cover_max_mul); cover property (cover_zero_mul); cover property (cover_neg_boundary); end这三条分别覆盖最大值相乘、零边界、有符号正负交叉。如果 cover 报告显示其中某条没有被命中说明证明过程中输入空间被约束得可能过窄需要回头检查 assume 是否限制过头了。JasperGold 的report -cover会把每条 cover property 的被命中次数列出来未命中的条目在报告中会标红这是判断验证收敛最直接的信号。读报告时我会看三个状态。proved 表示断言成立且没有反例cex 表示存在反例undetermined 表示超时未决。如果一个断言长期 undetermined我通常不会无限加大 timeout而是先检查是不是约束条件写得太弱导致求解器搜索空间爆炸或者把断言拆小先验证截断前的全精度乘积再单独验证截断逻辑分而治之。乘法模块还有个特常用的收敛手段是把输入位宽临时调小比如从 32 位调到 8 位跑一轮看断言是否依然成立、反例是否依然出现这能在不引入版本号或特殊算法的前提下快速暴露参考模型里的逻辑错误。我自己的习惯是在 regress 脚本里把 JasperGold 的 prove 和 cover 放在同一个任务中运行prove 全绿、cover 无未命中、溢出标志双向断言都 proved这才敢签验证完成。把参考模型直接放在断言模块里相比动态仿真平台省掉的测试用例数量相当可观但省掉的这些时间必须花在读报告和调约束上否则形式验证很容易跑出一个“全绿却没测到重点”的结果。希望这些路径和坑能让你在 JasperGold 验证乘法模块时少走几步弯路。本文还有配套的精品资源点击获取