简介：这份资源是Cadence JasperGold Sequential Equivalence Checking App的官方用户指南（2020.03版），面向从事集成电路形式验证的工程师、验证方法学研究者及芯片设计相关专业的高年级学生。它聚焦顺序等价检查这一核心场景，帮助读者理解如何在不同抽象层次（行为级、RTL级、门级）之间验证设计逻辑行为的一致性，适用于系统级验证、IP复用与综合后验证等环节。压缩包内仅含1个PDF文件，大小约3.21MB，内容涵盖验证环境搭建、检查任务创建与配置、约束条件设置、时序问题处理以及分析与调试等关键流程，并附有第三方组件许可与商标法律声明。目前已有294人学习。通过这份指南，读者可系统掌握JasperGold在形式验证中的操作要点，学习如何利用其高级功能优化验证过程，从而在芯片流片前更高效地发现逻辑不一致问题，提升验证效率与设计质量。
1. 从一份 JasperGold SEC 用户指南说起：形式验证到底怎么落地
如果你手里只有一份jaspergold_sec_userguide.pdf，第一反应大概率是：SEC 是什么，JasperGold 又能帮我干什么。SEC 全称 Sequential Equivalence Checking，顺序等价性检查，属于形式验证里专门解决「两个设计在时序上是否等价」的一类问题。它和组合等价性检查最大的区别在于，SEC 要处理寄存器、状态机、流水线这些带记忆的电路，不能只看当前输入输出对不对，还要看历史状态是否一致。JasperGold 是 Cadence 的形式验证平台，SEC 是它的一条独立 App，专门用来做 RTL 到 RTL、RTL 到网表、网表到网表之间的顺序等价性证明。这份用户指南解决的核心诉求很具体：怎么把两个设计读进来、怎么设时钟和复位、怎么跑证明、怎么读结果、怎么在证明不过的时候定位差异。适合谁看？前端设计工程师做 ECO 后想确认没改坏功能，验证工程师做 RTL 与综合网表比对，以及后端工程师在门级网表上做等价性签核。下面我按实际跑通一条 SEC 证明的路径，把这份指南里最值得先吃透的部分拆开讲。
2. 跑通第一条 SEC 证明：从读设计到出结果的最小闭环
2.1 先搞清楚 SEC 和 LEC 的边界在哪
很多人第一次接触 SEC 会把它和 LEC（Logic Equivalence Check）混在一起。LEC 通常指组合等价性检查，工具把两个设计切成一个个比较点，只证明对应比较点的布尔函数一致。SEC 则把时序元素纳入证明范围，工具需要建立两个设计的状态映射关系，然后证明从初始状态出发，任意输入序列下两个设计的输出和状态都一致。这个区别直接决定了你读设计的方式：LEC 可以只读网表不读 RTL，SEC 一般要求两边都有明确的时钟和复位定义，否则工具无法建立初始状态。
JasperGold SEC App 的底层证明引擎和 JasperGold 其他 App 共享，但 SEC 有自己的命令集和流程。用户指南里反复强调的一点是：SEC 不是仿真，不需要 testbench，但需要你告诉工具哪些信号是时钟、哪些是复位、哪些是常数。这些信息如果给错，工具要么报错退出，要么给出一个看起来通过但实际无意义的结论。我一般会在读设计之前先列一张表，把两个设计的时钟域、复位极性、常数引脚全部对齐，再开始写脚本。
2.2 最小命令集：读入、设时钟、跑证明
下面这段脚本是我在 JasperGold SEC 里跑通一条 RTL 对 RTL 等价性证明的最小命令集。假设左边是 golden 设计golden.v，右边是 revised 设计revised.v，顶层模块名都是top，时钟clk，复位rst_n低有效。
# 启动 JasperGold SEC App analyze -sv09 golden.v analyze -sv09 revised.v # 分别精化两个设计，指定顶层模块 elaborate -top top -sva -create_related_asserts # 设置时钟和复位，注意两边都要设 clock clk reset -expression {!rst_n} # 指定 golden 和 revised 的对应关系 set_sec_golden -module top set_sec_revised -module top # 跑 SEC 证明 sec -all这段脚本里每一步都有讲究。analyze只做语法分析和设计库加载，不建立层次；elaborate才真正展开设计，-sva打开 SystemVerilog 断言支持，-create_related_asserts会在后续证明中自动生成一些辅助断言。clock和reset必须两边都设，而且复位表达式要写清楚极性，!rst_n表示低有效。set_sec_golden和set_sec_revised用来告诉工具哪边是参考设计、哪边是待验证设计，如果两个设计顶层名不同，这里要分别指定。最后sec -all会启动所有比较点的证明，工具自动做状态映射和归纳证明。
跑完之后，工具会输出一个总结表，列出每个比较点的状态：proven、cex（反例）、undetermined。proven 表示等价性成立，cex 表示找到反例，undetermined 表示证明没跑完，通常是状态空间太大或者约束不够。第一次跑大概率会有 undetermined，这很正常，需要加约束或者调证明策略。
2.3 参数怎么调：时钟、复位、常数和黑盒
SEC 证明能不能收敛，八成取决于时钟复位和常数设置对不对。用户指南里有一节专门讲 clock 和 reset 的多种写法，我挑最常用的几种列在下面。
| 参数 | 作用 | 常见写法 | 注意点 |
|---|---|---|---|
| clock | 指定时钟信号 | clock clk | 多时钟域要分别指定，不能只写一个 |
| reset | 指定复位条件 | reset -expression {!rst_n} | 表达式要覆盖所有复位路径 |
| constant | 固定常数引脚 | constant -sig mode 1'b0 | 只对真正不变的信号用，别乱加 |
| blackbox | 处理黑盒模块 | blackbox -module mem_model | 黑盒模块的输出会被当成自由变量 |
| sec | 启动证明 | sec -all | 可以指定单个比较点，如sec -map |
constant这条命令特别容易翻车。有人为了让证明快点过，把一些模式选择信号直接固定成常数，结果证明通过了，但实际电路在另一种模式下行为不一致。我的血泪经验是：只有确认在等价性检查范围内该信号确实不变，才用 constant，否则宁可让它自由，让工具去证明。
blackbox处理的是设计中例化的存储器、模拟 IP 或者第三方加密模块。黑盒模块的输出会被工具当成自由变量，这意味着如果两个设计对黑盒模块的使用方式不同，SEC 可能证明通过但实际不等价。常见做法是给黑盒模块加一个简单的行为模型，或者用assume约束黑盒输出的行为范围。
2.4 证明不过怎么办：读反例和定位差异
证明不过的时候，工具会给出一个反例波形，显示从初始状态开始，经过多少个周期后两个设计的输出出现差异。读反例是 SEC 调试的核心技能。我一般按这个顺序看：先看反例长度，如果只有一两个周期，大概率是复位或者初始状态没对齐；如果几十个周期，可能是某个状态机或者计数器行为不一致；如果几百个周期，可能是存储器初始化或者流水线深度差异。
定位差异的常用手段是在反例波形里找第一个出现差异的信号，然后往回追它的驱动逻辑。JasperGold 提供sec -map命令可以查看工具自动建立的状态映射关系，如果映射错了，证明肯定过不了。另一个命令是sec -compare，可以指定只比较某几个输出或者内部信号，缩小排查范围。
如果反例看起来像是工具误报，先检查约束是不是给少了。SEC 证明是在所有可能的输入序列下进行的，仿真里没遇到的场景工具都会去试。加约束的时候要小心，约束太强会让证明变得无意义，约束太弱又收敛不了。我一般会先不加约束跑一遍，看看反例是不是真实存在的差异，再决定加什么约束。
3. 把 SEC 嵌进日常流程：脚本化、回归和签核标准
3.1 用 Tcl 脚本把重复劳动吃掉
SEC 证明很少只跑一次。ECO 之后要跑，综合之后要跑，门级网表回来还要跑。每次手动敲命令不现实，也不利于回归。我一般会把整个流程写成一个 Tcl 脚本，用变量控制设计路径、顶层名、时钟复位名，然后通过命令行参数传入。
# sec_run.tcl - 参数化 SEC 脚本 set GOLDEN [lindex $argv 0] set REVISED [lindex $argv 1] set TOP [lindex $argv 2] set CLK [lindex $argv 3] set RST_N [lindex $argv 4] analyze -sv09 $GOLDEN analyze -sv09 $REVISED elaborate -top $TOP -sva clock $CLK reset -expression "!$RST_N" set_sec_golden -module $TOP set_sec_revised -module $TOP # 设置证明策略，先跑快速模式 set_sec_method -fast sec -all # 如果有 undetermined，再跑完整模式 if {[sec -status -count undetermined] > 0} { set_sec_method -complete sec -all } # 输出报告 report_sec -summary -file sec_report.rpt这个脚本的关键点在于set_sec_method。-fast模式用较少的资源快速跑一遍，适合日常回归；-complete模式会花更多时间做完整证明，适合签核。report_sec生成报告，方便后续自动解析。实际项目中，我会把这个脚本挂到 Jenkins 或者本地 Makefile 里，每次 RTL 有改动就自动跑一遍。
3.2 回归策略：哪些比较点必须过，哪些可以放
SEC 证明的比较点数量可能很多，尤其是大型 SoC 设计，几千个比较点很正常。全部跑 complete 模式不现实，时间成本太高。我的做法是分层：第一层是顶层输出和关键状态寄存器，这些必须 complete 证明通过；第二层是内部模块的等价性，可以用 fast 模式先筛一遍，有问题的再单独跑 complete；第三层是黑盒模块周边的逻辑，如果黑盒模型本身不可信，这部分证明结果只能作为参考。
用户指南里提到 SEC 支持-map和-compare两种模式。-map模式让工具自动建立状态映射，适合两个设计结构相似的情况；-compare模式需要手动指定比较点，适合结构差异较大的情况。我一般先用-map跑一遍，如果 undetermined 太多，再切到-compare手动指定关键比较点。
回归的时候还要注意版本管理。golden 设计和 revised 设计的版本要明确记录，否则证明通过了也不知道是哪个版本对哪个版本。我习惯在脚本里加一行puts "Golden: $GOLDEN, Revised: $REVISED"，把版本信息打到日志里。
3.3 签核标准：什么情况下可以签字
SEC 签核不是所有比较点都 proven 就完事了。我一般会看三个指标：proven 比例、undetermined 比例、cex 数量。proven 比例要接近 100%，undetermined 要逐个分析原因，cex 必须全部清零或者有明确的 waiver 理由。waiver 的理由不能是「看起来没问题」，必须是「该比较点对应的逻辑在本次 ECO 中未改动」或者「该差异已被仿真覆盖且确认无害」。
还有一个容易被忽略的点：SEC 证明通过不代表设计功能正确。SEC 只证明两个设计等价，如果 golden 设计本身有 bug，revised 设计继承了这个 bug，SEC 照样通过。所以 SEC 是签核流程中的一环，不是全部。我一般会把 SEC 和仿真、Lint、CDC 检查一起看，任何一个环节有疑问都要追到底。
4. 避坑与排查：SEC 证明里最容易翻车的五个地方
4.1 现象：证明秒过，但仿真对不上
原因：约束给太强，把关键输入固定成了常数，工具在受限空间里证明通过，实际电路行为被掩盖。 解决：去掉所有非必要的 constant 和 assume，重新跑一遍。如果去掉之后证明不过，说明之前的通过是假象。我一般会保留一份「无约束」的证明结果作为基准，任何加约束的证明都要和基准对比。
4.2 现象：工具报错「cannot find clock」或者「reset expression invalid」
原因：时钟或复位信号名写错，或者复位表达式里用了工具不支持的语法。SEC 对复位表达式的解析比较严格，!rst_n可以，rst_n == 1'b0有时候会报错。 解决：先用get_designs和get_pins确认信号名存在，复位表达式尽量用简单的逻辑非或者逻辑与。如果复位有多个来源，用-expression把所有条件写全。
4.3 现象：undetermined 数量很多，证明跑不完
原因：状态空间太大，或者设计里有大量黑盒模块，工具无法建立有效的状态映射。 解决：先检查黑盒模块是不是必须的，能给行为模型就给行为模型。然后尝试set_sec_method -fast先跑一遍，看哪些比较点容易过。对于确实跑不完的比较点，可以用sec -compare手动指定关键信号，缩小证明范围。如果还是不行，考虑用assume加一些合理的输入约束，但一定要记录约束理由。
4.4 现象：反例波形里两个设计输出差异出现在复位释放后的第一个周期
原因：复位释放的时序不一致，或者两个设计的初始状态不同。SEC 默认假设两个设计从相同的初始状态开始，如果复位逻辑有差异，第一个周期就会出问题。 解决：检查两个设计的复位树是不是完全一致，复位释放是否同步。如果复位逻辑确实不同但功能等价，可以用reset -sequence指定复位序列，让工具按指定的顺序释放复位。
4.5 现象：门级网表 SEC 证明大量 undetermined
原因：综合后的网表里时钟树、复位树被改过，或者出现了 RTL 里没有的锁存器、三态门。门级网表的信号名和 RTL 也不一样，工具自动映射容易出错。 解决：门级 SEC 一般需要额外的映射文件，把 RTL 和网表的对应关系写清楚。用户指南里有一节讲-map_file的格式，我一般会从综合工具导出映射关系，再手动补充关键寄存器。另外门级网表的常数引脚更多，需要仔细检查哪些是真正的常数、哪些是测试逻辑。
5. 进阶技巧：用 SEC 做 ECO 影响分析和形式化调试
5.1 用 SEC 量化 ECO 改动的影响范围
ECO 之后跑 SEC，除了看通过不通过，还可以看哪些比较点从 proven 变成了 cex 或者 undetermined。这个变化集合就是 ECO 改动的影响范围。我一般会在 ECO 前后各跑一次 SEC，把两次报告做 diff，重点关注新增的 cex 和 undetermined。如果 ECO 只改了一个模块，但 SEC 显示十几个不相关的比较点出了问题，大概率是改动引入了跨模块的副作用，需要回头检查。
# 对比两次 SEC 报告，找出状态变化的比较点 set before [read_report sec_before.rpt] set after [read_report sec_after.rpt] foreach point [dict keys $after] { set old_status [dict get $before $point] set new_status [dict get $after $point] if {$old_status ne $new_status} { puts "Changed: $point $old_status -> $new_status" } }这段脚本把两次报告读进来，逐比较点对比状态。实际用的时候可以把输出重定向到文件，再人工筛选。重点看 proven 变 cex 的比较点，这些是 ECO 引入的真实差异；proven 变 undetermined 的可以放一放，可能是证明资源不够。
5.2 形式化调试：从反例反推 RTL 差异
SEC 给的反例波形是形式化调试的起点。我一般会把反例波形导出成 VCD，然后在波形查看器里和 RTL 仿真波形对比。如果反例里的信号在 RTL 仿真里也出现了同样的值，说明差异是真实的；如果反例里的信号在 RTL 仿真里根本不可能出现，说明约束不够，工具探索到了非法状态。
另一个技巧是用sec -trace命令让工具输出证明过程的详细信息，包括状态映射、归纳步骤、哪些断言被使用。这个输出很长，但有时候能发现工具自动映射的错误。比如工具把 golden 设计的某个寄存器和 revised 设计的另一个寄存器映射到了一起，证明就会莫名其妙地失败。这时候手动指定映射关系比自动映射更可靠。
5.3 我自己的习惯：每次 SEC 都留一份「后悔药」
跑 SEC 最怕的是证明过了，但过了一段时间发现当时的约束有问题，想复现却复现不了。我的习惯是每次跑 SEC 都把脚本、约束文件、报告、反例波形全部归档到一个带时间戳的目录里。脚本里用变量控制所有路径，不写死任何绝对路径。这样半年后回头看，还能一键复现当时的证明环境。
还有一点：SEC 证明通过之后，不要急着删掉中间文件。JasperGold 的证明数据库有时候需要重新加载才能查看细节，删了就得重跑。我一般会保留最近三个版本的证明数据库，更早的再清理。
希望这些从用户指南里拆出来的实操细节，能帮你在第一次跑 JasperGold SEC 的时候少翻几次车。
本文还有配套的精品资源，点击获取
