简介：Cadence官方发布的JasperGold低功耗验证应用用户指南，面向IC验证工程师与芯片设计人员，针对多电源域、时钟门控等低功耗设计的形式验证难题，提供系统化指导。资源包共含1个PDF文件，大小约936KB，正文围绕工具介绍、低功耗建模、验证环境搭建与完整流程、命令与脚本、案例研究、错误调试、性能优化等模块展开，结构清晰，便于查阅。已有180人学习下载，适合需要将低功耗形式验证落到实际项目的工程师，也可作为形式验证初学者的系统参考。借助该指南，读者可掌握活动、睡眠、待机等电源状态下的行为验证方法，深入理解电源门控、多电压域、时钟门控等技术的验证要点，并学会结合LSF等外部工具优化数据分析和报告生成，从而在芯片设计早期发现缺陷，降低修复成本。
1. JasperGold LPV 不是“旧属性验证”：一份用户指南里最容易被误读的概念
JasperGold LPV 用户指南，听起来像在教人验证“老代码”，但 Legacy Property Verification 里的 legacy 指的是“RTL 里已经存在的断言”，而不是过时的验证方法。它解决的是仿真验证最尴尬的一类问题：设计里塞了几百条 SVA，回归日志全绿，但谁也不敢保证那些断言真的被触发过。LPV 做的事情，是把 RTL 里这些既有断言直接交给 JasperGold 的形式化引擎，用 prove 命令在完整状态空间里穷举验证路径，不需要从零搭建形式化 testbench，也不需要为每条断言单独写一套激励。适合每天被仿真回归淹没、想引入 formal 又怕太重、或者被要求“所有断言必须有形式化证明”的验证工程师和设计工程师。这份指南翻着厚，真正决定你能不能跑通项目的，其实是一条主线加三类参数，下面按这条主线展开。
2. 读懂 LPV 的验证主线：从 setup 文件到 prove 命令的执行路径
LPV 这套流程的核心路径只有四步：读入 RTL、建立层次、建模环境、执行证明。用户指南里几百页的内容，绝大多数是围绕这四步的变体——不同的读入方式、不同的约束写法、不同的证明策略。把这四个动作钉在脑子里，再看任何一章都不容易迷路。
2.1 LPV 和等价性检查不是一回事：为什么既有断言还需要形式化证明
很多团队已经有等价性检查（SEC/EC）流程，于是看到 LPV 的第一反应是“我们不是已经在做 formal 了吗”。等价性检查证明的是两个电路逻辑一致，它不关心电路行为对不对——参考模型错了，检查照样通过。LPV 证明的是设计行为本身是否满足断言，这是两个完全不同的验证目标。
另一个容易被忽略的点是：RTL 里那些断言，在仿真环境下经常出现 vacuous pass。比如一条 FIFO 溢出断言assert property (cnt < DEPTH)，如果回归激励里 FIFO 从来没有接近满过，这条断言每一轮仿真都是“通过”的，但它从未验证过真正的边界行为。LPV 的价值就是把这类断言放进完整状态空间里证明，让“没触发过”变成“证明过”。这也是为什么 LPV 对已有大量 SVA 的设计价值最大——那些断言本身就是团队的经验沉淀，缺的只是一个能真正穷举的执行引擎。
2.2 最小 setup 文件：先读什么、后读什么、为什么这个顺序不能乱
LPV 的入口通常是一个 Tcl 脚本，JasperGold 把它叫做 setup 文件。最小可跑的结构是这样的：
# lpv_minimal.tcl # 先读 RTL 实现，再读断言文件，顺序影响 elaborate 的结果 read_verilog -r ../rtl/top.sv read_verilog -r ../rtl/cdc_sync.v read_verilog -sv ../rtl/top_assertions.sv # 建立顶层层次 elaborate -top top # 声明时钟和复位释放边沿 create_clock -name clk -period 10 reset -sequence {rst_n} -edge high # 复位释放后的稳定状态约束 assume { rst_n == 1'b1; }第一行read_verilog -r里的-r表示“只读入、不立即展开”。多个文件依次读完后，再由elaborate -top top统一建立层次，这是 LPV 最常见的批处理方式，能避免文件间例化顺序带来的麻烦。
read_verilog -sv是另一个关键开关。断言文件用了 SystemVerilog 的assert property语法，必须用-sv读入，否则工具会把 SVA 当成注释或非法语法跳过，后续 prove 直接报 property not found。create_clock定义形式化引擎的时间基准，周期数值本身不一定要和仿真完全一致，但时钟必须存在，否则所有 concurrent assertion 都没有采样事件。reset -sequence {rst_n} -edge high这行容易写反：rst_n 是低有效信号，复位释放时从 0 变 1，所以-edge high描述的是“复位结束”的边沿，不是复位生效的边沿。
提示：如果设计里有多个异步复位域，
reset -sequence要分别写，不能只约束一个。漏掉任何一个复位域的初始化，反例里就会出现莫名其妙的 X 态，debug 时极难定位。
最后一行assume { rst_n == 1'b1; }的作用是把证明起点固定在复位释放后的稳定状态。不写这行，prove 会把复位期间的未初始化行为也纳入搜索，状态空间变大不说，还容易给出仿真里根本不会出现的反例。
2.3 prove 命令与日志：Proved、Failed、Inconclusive 分别代表什么
setup 文件准备好之后，LPV 的执行通常有两种方式：交互式的jg界面，或者批处理模式。回归环境里一般用批处理：
jg -batch -do lpv_minimal.tcl -log run.log跑完之后打开run.log，每个属性会对应三种结局之一。
Proved表示在给定的状态空间内没有找到违反路径。注意“给定”两个字——如果约束写得不够，这个 Proved 的覆盖范围是打了折扣的；如果约束写得过强，它甚至可能是 vacuous pass。Failed表示引擎找到了一条从初始状态到违反点的反例路径，日志里会给出具体的输入序列和周期。Inconclusive是 LPV 里最常见的“非结论”：引擎在分配的时间或深度内没有搜完全部状态，既没证明也没推翻。
对 Inconclusive 的处理不是直接加时间重跑，而是先看日志里的尽力信息。JasperGold 会输出类似 “trying to prove ... bound reached” 的提示，告诉你它探索到了多深的 cycle。如果属性本身只涉及 3 拍以内的时序逻辑，但 bound 已经跑到 50 拍还没结论，那通常是状态空间爆炸，不是深度不够。这时应该回到约束和属性本身去调，而不是把set_prove_time_limit从 1800 改成 18000。盲目加时间是最常见的资源浪费，后面第 6 章会细说怎么调。
3. 用 LPV 跑通第一个 Property：属性分类、约束建模与参数设置
跑通 prove 很容易，跑出“有意义”的证明很难。这一章把属性类型和环境建模拆开讲，最后给出一套可以直接照抄的最小工程。LPV 不是把 assert 丢给工具就完事，约束的质量直接决定证明结果可不可信。
3.1 LPV 能验证哪几类属性：assertion、cover、restrict 的实际差异
SVA 里常见的属性指令在 LPV 下的角色完全不同，用错会直接导致误判。
| 属性类型 | 典型写法 | LPV 里的角色 | 典型用途 |
|---|---|---|---|
| assertion | assert property (...) | 证明目标 | FIFO 满空、协议时序、状态机安全 |
| cover | cover property (...) | 可达性检查 | 确认某个场景能否被激励到达 |
| restrict | restrict property (...) | 输入约束 | 把输入限制在合法协议范围内 |
assert是证明对象，LPV 要为它穷举所有可能的输入序列。cover不是证明目标，它告诉引擎“帮我找一条能到达这个状态的路径”——这是评估约束质量最重要的工具。restrict property把输入空间剪掉一部分，不会成为证明目标，但它会影响所有 assertion 的结论：restrict 剪掉的路径如果恰好是 bug 所在的路径，prove 照样全绿。
这三者的配合关系是：restrict 定义环境的合法输入，assert 定义设计必须满足的行为，cover 反过来检查 restrict 有没有把不该剪的路径剪掉。一个断言如果 Proved，但它的前提条件在 cover 下不可达，这个 Proved 就是 vacuous pass，没有任何验证价值。后面第 5 章会看到这种假绿的危害。
另外要区分 concurrent assertion 和 immediate assertion。LPV 证明的对象主要是 concurrent assertion（assert property这种带时钟事件的断言）。写在 always 块里的 immediate assertion 虽然也能读入，但形式化语义下需要额外推导采样时刻，建议在 LPV 项目中尽量把关键属性写成 concurrent assertion，减少工具解释的歧义。
3.2 环境建模：把仿真 testbench 翻译成 assume 和 restrict
LPV 不需要 testbench，但必须告诉引擎哪些输入序列是合法的。仿真里靠 force、initial 块、总线功能模型实现的约束，在 LPV 里全部要翻译成 assume 或 restrict。这一步做得越贴近真实环境，prove 的结论越可信。
常见的做法是：协议规定的合法输入用restrict property写进断言文件，跨模块的环境假设用assume写在 setup 脚本里。例如 AXI 总线 burst 长度受限：
restrict property (len inside {[0:7]}); restrict property (valid |-> ready within [1:3]);第一行限制 burst 长度只能在 0 到 7 之间，第二行限制 valid 拉高后 ready 必须在一到三拍之内到达——这类约束来自协议，是设计本身假设的合法输入范围。如果这些约束缺失，prove 会把“总线发来一个长度为 15 的 burst”也纳入搜索，反例自然容易找，但那个反例在真实系统里根本不会出现，属于假失败。
约束建模最忌两件事。第一件是“把断言当约束用”：如果把a |-> b既写成assert property又写成restrict property，prove 必定通过，因为引擎只会搜索满足前提 a 的输入，而你的断言恰好就是那个前提——这是最典型的自证陷阱。第二件是“约束覆盖了错误的时间范围”：所有 assume 必须写在create_clock和reset之后，否则工具无法把假设绑定到正确的时钟事件上，约束可能完全没生效。
提示：LPV 里有一个检查约束质量的笨办法：把要 prove 的属性临时改成 cover。如果 cover 失败，说明约束或实现让这个场景根本不可达；如果 cover 通过但 assert 失败，才是真正的问题。
3.3 一个可照抄的最小工程：从 jg 启动到 prove 出结果
把前面的内容拼起来，一个完整的 LPV 最小工程如下。RTL 和断言文件分开读，约束独立成段，两个属性分别 prove：
# lpv_minimal.tcl read_verilog -r ../rtl/top.sv read_verilog -r ../rtl/cdc_sync.v read_verilog -sv ../rtl/top_assertions.sv elaborate -top top create_clock -name clk -period 10 reset -sequence {rst_n} -edge high # 环境约束 assume { rst_n == 1'b1; } restrict property (len inside {[0:7]}); restrict property (valid |-> ready within [1:3]); # 证明目标 set_prove_time_limit 1800 prove -property top.a_fifo_never_overflow prove -property top.a_state_onehot启动命令保持不变：
jg -batch -do lpv_minimal.tcl -log run.log这里有两个刻意设计。第一个是分两条prove命令而不是直接prove -all。开发期分开跑能快速定位是哪个属性撑爆了状态空间；等每个属性都能稳定收敛，再在回归里改成prove -all统一管理。第二个是set_prove_time_limit 1800——LPV 不是“跑多长时间”的问题，而是“分配多少资源给引擎”。1800 秒是经验值，超过这个值还没收敛，继续加时间通常也收不了，应该回去调约束。
如果top.a_fifo_never_overflow报 property not found，先不要怀疑名字写错，回去确认read_verilog -sv有没有加、断言文件有没有被读入。用report_properties列出当前设计中所有已识别的属性名，对比一下实际层次名，尤其注意generate块会改变属性全名。
4. 反例分析实战：JasperGold 报告 failed 之后的四个调试动作
真正让新手劝退的不是 setup 报错，而是prove回了一个Failed——打开反例波形一看，完全不像仿真里见过的样子。这不是工具坏了，而是形式化反例的生成逻辑和仿真激励本来就不一样。按顺序做四个动作，大部分失败都能定位。
4.1 LPV 反例为什么看起来不像仿真波形
仿真波形里的激励是人写的，有业务场景的逻辑；形式化反例是引擎为了最快违反属性找出来的输入组合，它不在乎这条路径在业务上合不合理。反例里的输入可能组合了“你没见过的 burst 长度 + 奇怪的 valid/ready 时序 + 某个寄存器还没初始化的 X”，看起来像是工具在胡闹，实际上是约束没把这些非法输入排除干净。
所以拿到反例的第一反应不要是“工具找错了”，而是“我少约束了什么”。反例里最前面几个 cycle 往往藏着答案：输入信号是不是超出了 restrict 限定的范围、复位信号是不是处于中间态、跨时钟域的信号是不是没有同步约束。把约束补齐，再跑 prove，反例会往后缩，直到缩到一个真正符合协议的行为序列。
4.2 第一步：判别是“属性错”还是“约束错”
prove 失败有两种来源：属性本身写错了，或者约束环境不对。区分的办法是把属性改成 cover 再跑一次：
cover -property top.a_state_onehot如果 cover 失败，说明在当前的约束环境里，属性描述的场景根本不可达——不是设计错了，是约束过强或者属性描述的状态本身就不存在。如果 cover 成功，说明场景可达到，那么 assert 失败就是设计行为确实有问题。这一招能避免大量无效 debug，应该在每个 Failed 属性上先执行。
另一种判别方式是反向操作：把可疑的 restrict 约束临时注释掉，重新 prove。如果属性从 Failed 变成了 Inconclusive，说明这条约束恰好把设计引向 bug 的路径剪掉了——约束过强；如果注释掉之后还是 Failed，且反例路径变了，说明 bug 是真实存在的，只是原先的反例路径藏在被剪掉的空间里。无论哪种结果，都能给下一步指个方向。
4.3 第二步：读懂反例波形里的 X 态语义
反例波形里出现 X，是 LPV 新手最容易翻车的地方。仿真里 X 通常来自未初始化寄存器或三态总线，而形式化引擎对 X 的处理完全不同：未初始化信号在形式化语义下可以取任意值，引擎会主动尝试 0 和 1 两种取值来找反例。这意味着反例可能用到了“仿真里永远选不到”的输入组合。
处理 X 态反例，先检查复位建模覆盖了哪些信号。如果设计有独立的异步复位域，reset -sequence没写全，该域内的寄存器在 prove 起点就是自由的，X 会一路传播到断言。补全复位序列后，在 setup 里加一句：
assume { rst_n == 1'b1; }把起点固定在复位释放后的稳定状态。跨时钟域的 X 反例单独处理——两个异步时钟域之间的信号需要同步假设，否则引擎会构造出理论上存在的亚稳态路径。通常做法是对跨域信号加restrict property约束其在采样时刻稳定，或者直接在证明中排除跨域路径。仿真里看不到的 X，在形式化里是真实存在的反例来源，不能无视也不能照单全收。
4.4 第三步：用 visualize 和 report 命令定位根因
定位反例的具体违反点，JasperGold 提供两个最常用的命令：
report_failing_properties visualize -property top.a_fifo_never_overflowreport_failing_properties列出当前所有失败属性，以及每条属性对应的输入约束集合，用来确认“是不是所有该有的约束都生效了”。visualize打开反例波形视图，波形会从初始状态开始，一直播放到违反点。
看反例波形的技巧是从违反点往前倒着看，不要从起点往后顺着看。违反点那一拍之前的两到三个周期，信号一定已经偏离了属性描述的正确行为。比如属性要求valid |-> ready within [1:3]，反例在第五拍报 fail，那往前数三拍，看 valid 拉高之后 ready 有没有在窗口内响应。盯着违反点看永远找不到原因，因为它只是压垮骆驼的最后一根稻草。
5. LPV 常见问题排查：5 个让 prove 卡死或误报的实际场景
LPV 用久了会发现在一个固定的“问题集”里打转：要么不收敛，要么假绿，要么断言读不进来。下面五个场景是我在多个项目里反复遇到的，每条按现象、原因、解决三个层次说清楚。
5.1 现象：prove 停在 Inconclusive，日志反复出现 “trying to prove”
状态空间爆炸是 LPV 最常见的 Inconclusive 原因，典型特征是日志里引擎一直在尝试，但 bound 推进极慢，时间耗完也没得出结果。最容易撑爆状态空间的是大位宽数据通路——一个 32 位计数器参与的比较逻辑，展开后的状态数是天文数字。
解决思路不是加时间，而是缩小搜索空间。第一，如果协议本来就限定了计数范围，用restrict property (cnt < 16)这类约束把无关状态剪掉。第二，把长属性拆成短属性：一个跨越五个周期的复杂断言收敛难度远高于两个各跨两拍的断言，中间用中间信号打一拍。第三，检查set_prove_effort的级别，开发期用 quick/medium 足够，exhaustive 留到最终回归。有些项目为了早出结果把 effort 一直拉满，结果反而是在错误的方向上浪费算力。
5.2 现象：属性全部 Proved，回头却发现设计有 bug——vacuous pass
这是 LPV 最危险的结果，因为它看起来全绿，日志没有任何告警，直到芯片回来或后仿才暴露问题。原因几乎总是同一个：属性的前提条件被约束环境剪掉了，引擎没有找到任何能触发前提的输入，于是该属性被认为是“证明成功”。
排查方法是为每一条重要的 assert 属性配套写一条 cover，单独检查它的前提可不可达。例如断言是assert property (a |-> b)，那 cover 就应该写cover property (a)，然后跑：
cover -property top.c_antecedent_reachable如果 cover 失败，说明前提 a 不可达，这条 Proved 就是 vacuous pass。把“每个证明必须配一个可达性 cover”写进回归检查清单，是堵住假绿最有效的办法。这个习惯救过我一次，当时一条 FIFO 满的断言 Proved 了整整两周，cover 跑出来才发现 reset 约束把 FIFO 写入路径完全剪掉了。
5.3 现象：read_sa 读不到断言，prove 报告 property not found
property not found 九成是读入阶段的问题。断言文件用了 SystemVerilog 语法但没加-sv开关，文件被工具当成普通 Verilog 解析，assert property被跳过；或者断言写在 generate 块里，elaborate 后属性全名带上了 generate 实例名，和脚本里写的层次路径对不上。
解决按两步走。第一步确认读入方式：
read_verilog -sv ../rtl/top_assertions.sv如果断言是独立文件，也可以用断言导入命令注册到当前 design context。第二步用report_properties查看工具实际识别到的属性全名，对照脚本里的路径修正。develop 阶段不要用通配符匹配属性名，老老实实写全名，否则哪天 generate 参数变了，你会看到一个“找不到属性但也没报错”的假象。
5.4 现象：反例波形里出现 X，但 RTL 仿真里根本没有 X
问题出在初始状态建模。仿真中寄存器上电有确定的初值，形式化引擎对未初始化寄存器按自由变量处理，0 和 1 都可能取，引擎会特意选择能制造反例的取值，于是波形里就出现了仿真里不存在的 X 传播路径。
解决方法是把证明起点钉死在复位释放后的稳定状态。检查 setup 里的reset -sequence是否覆盖了所有复位域，再确认assume { rst_n == 1'b1; }已写入。如果设计里有跨时钟域路径，单独对异步信号加同步属性约束。处理完这些之后重新 prove，X 态反例如果消失，说明是初始化建模问题；如果还在，说明设计里存在真实的可配置 X 传播路径，这反而是个值得深挖的设计问题。
5.5 现象：多个属性一起 prove 很慢，单个却很快
分开 prove 每个属性都能在几十秒内收敛，放一起prove -all就挂到超时。原因是多个属性共享同一个证明上下文，引擎为每个属性展开的 BMC 逻辑会互相影响，状态空间不是加法而是乘法。
解决方法是把属性按模块或按功能分组，每组一个独立的 prove 命令，必要时拆成多个 elaborate 上下文。回归脚本里可以用循环统一管理：
foreach property_list { top.a_afifo_props top.a_state_props } { prove -property $property_list -timeout 1200 }开发期用这种分组方式，最终回归再跑全量prove -all。另一个经验是：如果某一个分组明显比其它组慢，那组里大概率有一条属性写得太宽，拆开排查往往能发现收敛瓶颈。
6. 收敛性调优：让 LPV 回归从“跑不完”变成“每天都能跑”
前面说了一堆 Inconclusive 和状态空间爆炸，最后落到一个具体的调优策略组合。LPV 回归能不能每天跑，不取决于机器多强，取决于你对 effort、timeout 和属性粒度的控制。
第一层是 effort 分级。开发期用set_prove_effort quick做冒烟，目标是快速暴露 Failed 和脚本错误；功能冻结后用set_prove_effort exhaustive做最终证明。不要一上来就跑 exhaustive，它会把引擎的探索策略推向“必须收敛”，在属性还没调稳时只会浪费算力和时间。
第二层是超时重跑策略。LPV 不是一次 prove 定终身，1800 秒 Inconclusive 之后，正确的动作是调约束、拆属性，再跑第二轮。我一般把 1800 秒定为单条属性的上限，超过就回到第 3 章的约束检查流程。加时间是最偷懒也最低效的做法，不加约束只加时间，相当于用三倍的算力给同一个状态空间爆炸擦屁股。
第三层是属性分解。长周期断言尽量拆成两段，中间用流水信号连接，这是 LPV 收敛性提升最明显的手段。我最早做 LPV 回归时，天真地把所有属性丢给 prove -all，日志绿了三天，最后发现三分之一是 vacuous pass。后来我把“每个证明必须配一个可达性 cover”写进团队的回归检查清单，假绿的问题才被真正堵住。LPV 的价值不在工具本身，而在你愿不愿意把约束环境当测试平台一样精心维护。希望帮到你。
本文还有配套的精品资源，点击获取
