简介这份资源是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 会把它和 LECLogic Equivalence Check混在一起。LEC 通常指组合等价性检查工具把两个设计切成一个个比较点只证明对应比较点的布尔函数一致。SEC 则把时序元素纳入证明范围工具需要建立两个设计的状态映射关系然后证明从初始状态出发任意输入序列下两个设计的输出和状态都一致。这个区别直接决定了你读设计的方式LEC 可以只读网表不读 RTLSEC 一般要求两边都有明确的时钟和复位定义否则工具无法建立初始状态。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 1b0只对真正不变的信号用别乱加blackbox处理黑盒模块blackbox -module mem_model黑盒模块的输出会被当成自由变量sec启动证明sec -all可以指定单个比较点如sec -mapconstant这条命令特别容易翻车。有人为了让证明快点过把一些模式选择信号直接固定成常数结果证明通过了但实际电路在另一种模式下行为不一致。我的血泪经验是只有确认在等价性检查范围内该信号确实不变才用 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 设计本身有 bugrevised 设计继承了这个 bugSEC 照样通过。所以 SEC 是签核流程中的一环不是全部。我一般会把 SEC 和仿真、Lint、CDC 检查一起看任何一个环节有疑问都要追到底。4. 避坑与排查SEC 证明里最容易翻车的五个地方4.1 现象证明秒过但仿真对不上原因约束给太强把关键输入固定成了常数工具在受限空间里证明通过实际电路行为被掩盖。 解决去掉所有非必要的 constant 和 assume重新跑一遍。如果去掉之后证明不过说明之前的通过是假象。我一般会保留一份「无约束」的证明结果作为基准任何加约束的证明都要和基准对比。4.2 现象工具报错「cannot find clock」或者「reset expression invalid」原因时钟或复位信号名写错或者复位表达式里用了工具不支持的语法。SEC 对复位表达式的解析比较严格!rst_n可以rst_n 1b0有时候会报错。 解决先用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 的时候少翻几次车。本文还有配套的精品资源点击获取