简介面向数字IC验证工程师及学习者源码包演示了使用JasperGold对基于Booth算法的乘法器模块进行形式化验证的完整流程。压缩包共7个文件约9KB包含RTL源码mul_top.v、C黄金参考模型mul.c、TCL验证脚本verify_mul.tcl以及README、TODO等说明文档可直观对照断言配置、时钟复位、virtual_net与proof_structure等关键步骤。已有126人学习适合希望快速上手JasperGold工具、理解乘法器验证建模思路的读者。通过研读这些文件能了解如何搭建黄金参考模型、编写自动化验证脚本并规避分支断言与验证空间优化中的常见问题。 提到JasperGold验证乘法模块我见过两种极端反应一种是这么简单的块还需要用形式验证吗另一种是形式验证太玄了还是老老实实跑UVM吧。这两种心态我都经历过最后是被一个真实bug打醒的。一个8位乘8位的流水线乘法器在随机仿真里跑了几千万拍都没出任何问题结果一旦切到有符号模式、输入恰好是0x80乘以0x01符号扩展错一位整个输出就不对了。这种边界在仿真里真的像大海捞针而形式验证相当于拿金属探测器扫整个海滩。JasperGold是Cadence旗下的RTL形式验证工具它把穷举证明这件事工程化了。用它来验证乘法模块覆盖的是所有输入组合而不是从测试用例里抽一小撮样本。这篇博文我会从为什么乘法模块适合形式验证讲起然后给出验证环境、断言源码、运行脚本以及我在真实项目里遇到的反例调试和不收敛问题。内容偏实践适合正在搭验证环境、想用JasperGold做数据通路验证的IC验证工程师也适合想从仿真思路切到形式验证的开发者。1. 乘法模块为什么是形式验证的主场仿真覆盖不了的数学边界1.1 乘法器不是一个a乘b那么简单芯片里的乘法模块代码上往往只是assign p a * b;一句话但综合出来的结构通常是Booth编码、Wallace树、进位保存加法器和最终进位传播加法器的组合。真正做验证的时候难点主要来自四个方向输入空间爆炸。一个16位乘16位的无符号乘法输入组合是2^32种仿真跑到天荒地老也只是一小撮样本如果是32位乘32位组合数是2^64在仿真世界里基本等于无穷大。符号扩展极容易错位。有符号/无符号混用、模式动态切换、输入在符号位上的特殊值只要有一处扩展位写错结果就偏得离谱。流水线时序耦合。valid_in到valid_out之间打了几拍中间如果还有反压、气泡数据对齐稍一疏忽验证环境自己先挂。边界值防御。0、1、-1、最大值、最小值这些值在乘法器里经常走不同的简化逻辑仿真覆盖率稍微差一点就漏掉。所以乘法器看起来简单实际上是一个典型的状态空间大但结构规则的数据通路模块。这类模块正是形式验证最擅长啃的骨头。1.2 形式验证的穷举到底是怎么做到的仿真验证本质上是在有限样本上做归纳推断你跑了三千万拍没问题不代表第三千万零一拍没问题。形式验证的思路完全不同把设计的可达状态空间建出来直接证明在所有这些状态里我的断言都不成立的话就是反例否则就是证明通过。JasperGold把这一套逻辑封装成了可用的EDA流程。我们读入RTL、告诉工具时钟和复位、把想证明的属性写清楚工具会组合使用BMC有界模型检验、SAT/SMT求解、BDD、抽象解释等引擎去遍历状态空间。对于乘法器这种数据通路现代求解器对算术约束有专门的处理方式JasperGold的数据通路求解器还能自动识别乘法结构所以往往能比传统穷举快几个数量级。但这种数学级验证也有边界如果设计是一个带几千个状态寄存器的复杂协议模块形式工具也扛不住。所以关键是把JasperGold用在刀刃上——乘法器就是最典型的刀刃之一。2. 验证环境搭建参考模型、JasperGold脚本与输入假设2.1 参考模型怎么选直接关系排查效率在JasperGold里验证乘法器我不建议把期望结果直接内联到SVA表达式里。比如assert property (product a * b)虽然能跑但一旦DUT内部有符号扩展、饱和处理、模式切换SVA里手写的期望值很容易和SystemVerilog的操作数位宽语义打架出了问题还不好定位。更稳的做法是例化一个纯组合的参考模型专门算教科书上的乘法结果然后用断言把DUT输出和参考模型输出做比对。参考模型的代码越简单越好核心逻辑就是// multiplier_ref.sv module multiplier_ref #( parameter W 16 )( input logic mul_signed, input logic [W-1:0] a, input logic [W-1:0] b, output logic [2*W-1:0] ref_product ); always_comb begin if (mul_signed) ref_product signed_ext(a) * signed_ext(b); else ref_product zero_ext(a) * zero_ext(b); end endmodule参考模型里可以用函数把符号扩展和无符号扩展写清楚function logic [2*W-1:0] signed_ext(input logic [W-1:0] v); signed_ext {{W{v[W-1]}}, v}; endfunction function logic [2*W-1:0] zero_ext(input logic [W-1:0] v); zero_ext {{W{1b0}}, v}; endfunction这一步看上去绕实际省了后面很多麻烦如果断言报反例你可以直接对比DUT输出和ref_product马上知道是DUT算错了还是验证环境对齐错了。2.2 主工程脚本让JasperGold先跑起来下面是一个可以直接套用的JasperGold主脚本。这里假设DUT叫multiplier参考模型和断言文件已经放在工程目录里。# scripts/jg_run.tcl set DESIGN multiplier set FILE_LIST [list \ ../rtl/multiplier.sv \ ../rtl/multiplier_ref.sv \ ../tb/multiplier_assertions.sv \ ../tb/multiplier_bind.sv \ ] read_file -format sverilog $FILE_LIST set_top $DESIGN clock clk -edge rising reset rst_n -async -active_low prove -property ap_mul_correct -timeout 1h report_proof -summary这里read_file把所有RTL和验证文件读进去set_top指定顶层是乘法的DUTclock和reset是关键告诉形式引擎时间语义否则它没法展开时序逻辑。跑完之后report_proof -summary会给出每个属性的证明状态。2.3 输入自由变量和约束别把形式验证当成仿真形式验证环境里的 a、b、valid_in 默认都是自由输入变量工具会自动量化所有可能取值不需要也不应该去给它们写随机激励。这正是形式验证和仿真最大的区别。但有些情况下确实需要加假设。比如valid_in不能和复位同时有效或者某些输入不会出现非法组合。这类约束用SVA的assume property写就行property p_no_valid_during_reset; (posedge clk) disable iff (!rst_n) !rst_n |- !valid_in; endproperty a_reset_input: assume property (p_no_valid_during_reset);不过我要提醒一句约束加得越少证明的范围越真实。很多时候你以为自己加的是合理约束实际把真实场景也约束掉了最后优雅地证明了一个假命题。3. 乘法器断言集把算对翻译成SVA语言3.1 核心数据通路断言DUT输出等于参考模型输出乘法的核心属性只有一个给定同一组输入DUT最终输出的product必须等于参考模型算出的ref_product。但时序上有个关键点DUT是流水线结构valid_in在第N拍拉高数据要到第N2拍才出现在product上。如果在断言里简单地写第N2拍product等于第N2拍的ref_product那比较的就是错误的数据对。我的做法是让参考模型也带一个与DUT同拍数的输入延迟管线保证ref_product在输出拍正好对应当前输入拍的历史数据。断言模块完整代码如下// tb/multiplier_assertions.sv module multiplier_assertions #( parameter W 16, parameter MUL_LATENCY 2 )( input logic clk, input logic rst_n, input logic valid_in, input logic valid_out, input logic mul_signed, input logic [W-1:0] a, input logic [W-1:0] b, input logic [2*W-1:0] product, input logic [2*W-1:0] ref_product ); property p_mul_correct; (posedge clk) disable iff (!rst_n) valid_in |- ##[MUL_LATENCY] (valid_out (product ref_product)); endproperty ap_mul_correct: assert property (p_mul_correct); endmodule这里ref_product来自参考模型的延迟对齐输出所以##[MUL_LATENCY]之后直接比较逻辑干净不会出现比对错数据的乌龙。3.2 握手协议断言乘法块不只是算数还是模块乘法模块在系统里不光是算乘法还承担着手握协议。如果它有valid/ready我最少会加两条property p_valid_out_handshake; (posedge clk) disable iff (!rst_n) valid_out |- ready_out; endproperty property p_valid_out_comes_from_valid_in; (posedge clk) disable iff (!rst_n) valid_out |- $past(valid_in, MUL_LATENCY); endproperty第一条保证valid_out拉高时下游一定允许接收第二条防止valid_out凭空出现每一项输出都必须对应一次有效的输入请求。这类断言在仿真里容易被忽略但却是形式验证最擅长的协议穷举场景。3.3 覆盖属性证明空间里的关键路径要能看到形式验证虽然全空间证明但我仍然习惯加覆盖属性用来确认那些关键的边界场景确实存在于可达状态空间里也用来排查约束是否过紧。常见的有cover property ((posedge clk) valid_in (a 0) (b 0)); cover property ((posedge clk) valid_in (a 1) (b 1)); cover property ((posedge clk) valid_in a[W-1] b[W-1]); cover property ((posedge clk) valid_in (a {1b1, {W-1{1b0}}}) (b 1));如果这些cover属性在中低步数下都hit不到就要回头检查是不是assume写得太死。4. 反例调试与不收敛真实项目中最耗时间的两个阶段4.1 一个CEX的完整追踪过程说说我印象很深的一次反例。当时验证一个16位带符号/无符号模式切换的乘法模块ap_mul_correct直接报了fail。打开JasperGold自动生成的反例波形信息非常清晰第10拍 valid_in1mul_signed1a16h8000b16h0001到第12拍 valid_out1product显示32h00008000而参考模型ref_product是32hffff8000。0x8000 在有符号模式下是 -32768乘以1应该还是 -32768即 32hffff8000。DUT输出 0x00008000说明它把 a 当成了无符号数。按这个方向查RTL代码问题很快浮出水面mul_signed 信号在DUT内部被第一级寄存器打了一拍导致第一级采集a和b时用的还是上一拍的mul_signed。如果输入数据到达和模式切换信号到达不在同一个节拍符号扩展就会错位。这种bug在随机仿真里需要精确命中模式切换瞬间 最低位为1 符号位为1的组合概率极低。但在形式验证里它就是反例波形的第一屏内容。这也是我后来坚持用形式验证验数据通路的原因。4.2 规模变大后证明不收敛的处理策略另一个项目是32位乘法器。直接把ap_mul_correct挂在顶层prove跑了一个多小时还没结果。大部分乘法器在JasperGold里都能直接收敛但结构特殊、位宽偏大的时候确实会卡住。我当时的处理分三步分层验证。把DUT内部的部分积生成逻辑单独提出来先证明每个部分积都和参考模型手工展开的部分积一致再做压缩树和最终加法的验证。把一个大乘法拆成几个小问题后每个子问题都轻松收敛。打内部截点。对内部大位宽总线设置cut point让JasperGold不要展开完整的乘法DAG用抽象引擎去处理路径上的大位宽数据。先BMC再抽象。用prove -semiformal -steps 2先跑有限步BMC让引擎在低深度范围内尽量找反例确认没有低级错误后再切抽象引擎做全空间证明。这套组合拳下来原来一小时的超时问题十几分钟就proven了。遇到乘法器不收敛不要急着加约束硬啃先想想能不能拆小、能不能抽象、能不能先抓浅层反例。4.3 断言过约束与欠约束的坑我见过最典型的过约束案例是有人为了仿真环境里的输入行为就是这样给valid_in加了拉高一拍必须拉低一拍的假设。结果看起来属性proven了实际上只是证明了特定节奏下的乘法器真实系统里连续两拍输入的场景完全没覆盖。判断标准很简单看报告里的覆盖情况。如果关键cover属性覆盖率始终很低大概率是约束太紧。欠约束则是反过来该加的模式互斥约束没加。比如DUT同时支持mul_signed和mul_unsigned两个模式信号实际硬件保证两者不会同时为1但SVA里如果没有用assume约束互斥证明过程就会去遍历那个实际不可能发生的非法状态产生一堆假反例或者让求解器浪费大量资源。5. 可复用的最小源码工程从目录到文件全量清单5.1 目录结构下面是一份可以直接复制的最小工程目录multiplier_formal/ ├── rtl/ │ ├── multiplier.sv │ └── multiplier_ref.sv ├── tb/ │ ├── multiplier_assertions.sv │ └── multiplier_bind.sv ├── scripts/ │ ├── jg_run.tcl └── output/5.2 DUT简化示例带流水线和模式切换的乘法器// rtl/multiplier.sv module multiplier #( parameter W 16, parameter MUL_LATENCY 2 )( input logic clk, input logic rst_n, input logic valid_in, input logic mul_signed, input logic [W-1:0] a, input logic [W-1:0] b, output logic valid_out, output logic [2*W-1:0] product ); logic [W-1:0] a_dly, b_dly; logic valid_dly1, valid_dly2; always_ff (posedge clk or negedge rst_n) begin if (!rst_n) begin a_dly 0; b_dly 0; valid_dly1 1b0; valid_dly2 1b0; end else begin if (valid_in) begin a_dly a; b_dly b; end valid_dly1 valid_in; valid_dly2 valid_dly1; end end function logic [2*W-1:0] sext(input logic [W-1:0] v); sext {{W{v[W-1]}}, v}; endfunction function logic [2*W-1:0] zext(input logic [W-1:0] v); zext {{W{1b0}}, v}; endfunction always_comb begin if (mul_signed) product sext(a_dly) * sext(b_dly); else product zext(a_dly) * zext(b_dly); end assign valid_out valid_dly2; endmodule5.3 参考模型的流水线对齐写法参考模型的关键不是乘法本身而是让参考输出和DUT输出在时间上严格对齐。做法是对输入a和b打同样的拍再在第二拍算乘法// rtl/multiplier_ref.sv module multiplier_ref #( parameter W 16, parameter MUL_LATENCY 2 )( input logic clk, input logic rst_n, input logic valid_in, input logic mul_signed, input logic [W-1:0] a, input logic [W-1:0] b, output logic [2*W-1:0] ref_product ); logic [W-1:0] a_dly, b_dly; always_ff (posedge clk or negedge rst_n) begin if (!rst_n) begin a_dly 0; b_dly 0; end else if (valid_in) begin a_dly a; b_dly b; end end function logic [2*W-1:0] sext(input logic [W-1:0] v); sext {{W{v[W-1]}}, v}; endfunction function logic [2*W-1:0] zext(input logic [W-1:0] v); zext {{W{1b0}}, v}; endfunction always_comb begin if (mul_signed) ref_product sext(a_dly) * sext(b_dly); else ref_product zext(a_dly) * zext(b_dly); end endmodule5.4 用bind把断言挂到DUT上在JasperGold里用SystemVerilog的bind把属性模块绑到DUT实例上是最推荐的注入方式不改动任何RTL代码// tb/multiplier_bind.sv bind multiplier multiplier_assertions #( .W(16), .MUL_LATENCY(2) ) u_assert ( .clk (clk), .rst_n (rst_n), .valid_in (valid_in), .valid_out (valid_out), .mul_signed (mul_signed), .a (a), .b (b), .product (product), .ref_product (multiplier_ref_inst.ref_product) );注意这里multiplier_ref_inst是参考模型的实例名实际使用时要保证参考模型在顶层设计中可见或者直接通过层次路径指定。5.5 主脚本与检查# scripts/jg_run.tcl set DESIGN multiplier read_file -format sverilog [list \ ../rtl/multiplier.sv \ ../rtl/multiplier_ref.sv \ ../tb/multiplier_assertions.sv \ ../tb/multiplier_bind.sv \ ] set_top $DESIGN clock clk -edge rising reset rst_n -async -active_low prove -property ap_mul_correct -timeout 1h report_proof -summary跑完之后如果看到ap_mul_correct Proven这条断言就通过了。如果某个属性是Falsifiable就用report_proof -counterexample导出反例波形按第4章的思路去追。最后再分享一个实战技巧JasperGold读大工程时如果参考模型、DUT、断言是分开的文件建议把路径写到list里一次性read_file不要分多次读能避免很多顶层识别的奇怪问题。另外第一次跑不建议追求全部proven先把ap_mul_correct这一条核心数据通路证明跑通再逐步往环境里加握手断言和覆盖属性。数据通路证明能过说明乘法器本身没问题协议断言证明能过说明模块作为子系统的行为符合契约。两条腿都站稳乘法模块的验证才算真正收口。本文还有配套的精品资源点击获取