企业官网建设流程全解析

简介：面向数字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{1'b0}}, 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指定顶层是乘法的DUT；clock和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拍拉高，数据要到第N+2拍才出现在product上。如果在断言里简单地写"第N+2拍product等于第N+2拍的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 == {1'b1, {W-1{1'b0}}}) && (b == '1));

如果这些cover属性在中低步数下都hit不到，就要回头检查是不是assume写得太死。

4. 反例调试与不收敛：真实项目中最耗时间的两个阶段

4.1 一个CEX的完整追踪过程

说说我印象很深的一次反例。当时验证一个16位带符号/无符号模式切换的乘法模块，ap_mul_correct直接报了fail。打开JasperGold自动生成的反例波形，信息非常清晰：第10拍 valid_in=1，mul_signed=1，a=16'h8000，b=16'h0001；到第12拍 valid_out=1，product显示32'h00008000，而参考模型ref_product是32'hffff8000。

0x8000 在有符号模式下是 -32768，乘以1应该还是 -32768，即 32'hffff8000。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 <= 1'b0; valid_dly2 <= 1'b0; 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{1'b0}}, 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; endmodule

5.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{1'b0}}, 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 endmodule

5.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这一条核心数据通路证明跑通，再逐步往环境里加握手断言和覆盖属性。数据通路证明能过，说明乘法器本身没问题；协议断言证明能过，说明模块作为子系统的行为符合契约。两条腿都站稳，乘法模块的验证才算真正收口。

本文还有配套的精品资源，点击获取