简介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 1b1; }第一行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 1b1; }的作用是把证明起点固定在复位释放后的稳定状态。不写这行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 里的角色典型用途assertionassert property (...)证明目标FIFO 满空、协议时序、状态机安全covercover property (...)可达性检查确认某个场景能否被激励到达restrictrestrict 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 assertionassert property这种带时钟事件的断言。写在 always 块里的 immediate assertion 虽然也能读入但形式化语义下需要额外推导采样时刻建议在 LPV 项目中尽量把关键属性写成 concurrent assertion减少工具解释的歧义。3.2 环境建模把仿真 testbench 翻译成 assume 和 restrictLPV 不需要 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 propertyprove 必定通过因为引擎只会搜索满足前提 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 1b1; } 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 1b1; }把起点固定在复位释放后的稳定状态。跨时钟域的 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 foundproperty 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 1b1; }已写入。如果设计里有跨时钟域路径单独对异步信号加同步属性约束。处理完这些之后重新 proveX 态反例如果消失说明是初始化建模问题如果还在说明设计里存在真实的可配置 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 的价值不在工具本身而在你愿不愿意把约束环境当测试平台一样精心维护。希望帮到你。本文还有配套的精品资源点击获取