简介《SPV_user_guide.pdf》是Cadence JasperGold形式验证工具中Security Path Verification应用的用户指南2019.12版面向芯片设计、验证与安全工程师用于在IC设计阶段建立并验证安全路径识别加密逻辑、访问控制及敏感数据传输等可能被攻击的薄弱环节。该资源共1个文件为PDF格式压缩包大小2.71MB内容紧凑且聚焦官方工具使用流程适合有一定形式验证基础并希望深化JasperGold应用的从业者参考。指南系统讲解了形式验证基本原理、安全路径定义方法、形式化属性编写、自动化工作流配置以及常见问题调试技巧并通过具体案例展示如何验证安全属性覆盖从工具设置到结果调试的完整流程。借助这些内容读者可以快速掌握Security Path Verification App的配置与执行方法在流片前发现潜在安全漏洞降低因安全缺陷导致的返工风险保护芯片知识产权和用户数据安全。目前已有108人关注学习是学习JasperGold安全路径验证功能的高价值参考资料。1. 形式验证在芯片设计里的真实姿态一份 SPV 用户指南能解决什么形式验证最容易被验证团队误解的一点是它不保证一定找得出 bug它保证的是“当一个性质被证明这条性质覆盖的输入空间内不存在 bug”。做 IC verification 的人大概率经历过这种时刻仿真回归跑了几百万拍什么都没炸签核前 formal 工程师丢过来一个 20 拍的反例直接把架构漏洞钉死。反过来一旦 formal 把某个属性证完同类场景的回归测试几乎不用再重复跑。SPV_user_guide.pdf 这份文档就是围绕这种验证范式展开的完整工具手册从断言怎么写、约束怎么加到证明引擎怎么选、反例怎么回放覆盖了把形式验证从 Demo 推到流片签核的全流程。它适合两类人一类是想接手 block 级 formal 签核的验证工程师另一类是仿真做了两三年、想给团队引入形式验证但一直被收敛问题劝退的人。看完你会明白formal 不是玄学只是需要一套比仿真更严格的输入纪律。2. SPV 验证前的三个基本概念断言、约束与可判定性2.1 断言在 formal 里不是注释SVA 断言与属性的完整语义仿真团队里常有一种惯性把断言当成“偶尔能拦一下违规的监视器”。在 sim 环境里断言挂了只是报一条 fail然后波形里翻一下没挂就当这条属性不存在。但在 SPV 这类形式验证工具里断言是证明的目标不是注释。工具会穷举它所有能到达的状态尝试找到让这条属性为假的路径。所以同一句断言在仿真里是“提示”在 formal 里是“判决”。举个最典型的请求-应答握手属性。总线模块里通常要求req 拉高后grant 必须在 1 到 2 拍内响应否则丢请求。写成 SVA 是这样property p_grant_after_req; (posedge clk) $rose(req) |- ##[1:2] grant; endproperty a_grant: assert property(p_grant_after_req);逻辑说明$rose(req)检测 request 信号的上升沿作为触发点|-是蕴含算子表示“当触发条件成立时后续时间窗内的表达式必须成立”。##[1:2] grant定义了从触发后的第 1 拍到第 2 拍这个区间内grant 信号必须为高。这个窗口是 formal 引擎实际扫描的深度范围。参数说明如果把##[1:2]改成##[0:2]含义会变成“触发当拍或者之后两拍内响应”这会扩大合法窗口可能放掉真正的问题。反过来收窄到##[1:1]会强制要求 grant 在下一拍立刻拉高很多实际设计根本做不到会报出一堆假反例。这种声明周期窗口是 SPV 证明时最影响收敛深度和结果可信度的参数之一。正确做法是先量一波仿真波形确认真实设计中 grant 的响应延迟分布再回来定这个窗口不要拍脑袋。2.2 assume 与 constraint约束缺失会让证明变成空转如果说断言定义了“设计必须满足什么”约束定义的则是“环境允许输入什么”。这两个概念在 formal 里是配套出现的。SPV 里用 constraint 机制来承担这个角色也叫 assume。缺少约束时formal 引擎会把所有输入端口都当作自由变量任意组合穷举结果就是大量反例来自实际上永远不会出现的输入序列——因为芯片外部环境根本不会那样驱动。spv constraint -label c_ready_in -port ready_in -mode assume -value free spv constraint -label c_valid_req -port req -mode assume -value guard spv constraint -label c_reset_settle -port rst_n -mode assume -value neg逻辑说明第一行把ready_in声明为自由但受约束的输入-mode assume告诉引擎这条端口不能随意翻转它的行为由后续约束限制第二行req被声明为必须遵守握手协议的输入第三行rst_n在证明期间默认保持为低电平复位态防止引擎把复位当成普通信号乱翻。参数说明-label 是约束的名字后续排查伪造反例时要靠它在日志里检索。-value 的三个取值free / guard / neg分别表示自由输入、受保护输入和固定电平输入。有一个容易翻车的细节复位约束在 formal 里通常要设置成-phase neg -assert 0即复位信号低有效在整个证明过程中先固定 0 一段时间让设计进入初态再释放。如果这里偷懒只用free引擎可能在复位窗口还没结束时就开始证明所有属性都会因为初态不稳定而报失败。2.3 有界证明与无界证明SPV 两种引擎在完备性上的取舍SPV 的证明引擎大致分两类有界引擎和无界引擎。有界引擎只扫描到指定深度找到反例就算完成找不到只能说明“在这个深度内没问题”不保证更深层没有 bug。无界引擎尝试覆盖所有可达状态证出来的结论是数学完备的付出代价是运行时间和内存可能暴涨。# 有界证明适合硬件加速器的有限深度检查 spv prove -scope a_grant -engine bounded -depth 50 # 无界证明适合核心控制逻辑的完备性验证 spv prove -scope a_grant -engine ic3 -timeout 3600逻辑说明第一个命令限制引擎只搜索 50 拍内的状态空间用于快速回归第二个命令换成 IC3 类算法尝试对全部可达状态证明属性-timeout 3600 表示超过 3600 秒自动终止避免验证任务无限期占用 license。参数说明-depth 的单位是时钟拍数不是时间。深度设置太小会漏掉长延迟的时序违例设置太大则每个状态点的展开逻辑会指数膨胀通常从 20 拍开始逐个加 10 拍观察资源占用。-engine 的选择直接决定证明结果类型用 bounded 证明成功日志里写的是 PASS但明确标注了深度范围用 ic3 证明成功日志里写的是 INDUCTIVE这才是真正可以用于签核的结论。很多团队签核时只看“PASS”不看引擎类型这是很危险的习惯。3. 搭建 SPV 验证环境三份文件与一组会骗人的命令3.1 目录与编译把 RTL 和断言按正确顺序喂给 SPV形式验证工程在落地上比仿真更敏感。仿真里文件读错顺序顶多编译告警formal 里读错顺序可能导致 binding 失效、属性找不到信号、甚至引擎直接把整个模块当成黑盒。SPV 工程的建议目录结构很简单RTL 源码一份、断言与绑定文件一份、约束脚本一份。这三份分开不要混在同一批sv文件里。spv read_file -f rtl/fifo_top.sv spv read_file -f rtl/fifo_ctrl.sv spv read_file -f bind/formal_bind.pkg.sv spv read_file -f props/properties.sva spv set_top -module fifo_top -binding formal_bind spv compile -O 2逻辑说明前四行按依赖顺序把设计文件、绑定模块、断言文件读入编译数据库。-binding参数指定了一个工具生成的实例模块它负责在验证阶段把属性安装到目标设计内部节点这是 formal 验证里最常见的做法——断言直接写成一个独立的包通过bind语句挂到 RTL 实例上不改动原始设计代码。参数说明-O 2是编译优化等级。等级 0 不优化编译快但后续证明可能因为冗余逻辑多而很慢等级 2 做逻辑综合级优化把常量传播、死逻辑清理掉证明效率高但编译时间翻倍。小模块用 -O 1 就行超过十万门的模块建议直接 -O 2否则后面证明任务跑起来内存占用差距非常明显。如果编译阶段报“signal not found”不要急着查波形先检查 binding 文件里的模块名和实例路径是否和 top 列表完全匹配。3.2 时钟与复位建模多时钟域和异步复位的声明顺序SPV 不会自动识别时钟。RTL 里写了always (posedge clk)工具能推断出 clk 是时钟但推断出的时钟域边界、相位关系都不够严谨直接用于证明会埋雷。正确做法是在编译完成后显式声明时钟和复位。spv add_clock -port clk -period 10ns -duty 50 spv add_clock -port ddr_clk -period 15ns -duty 50 -skew 2ns spv add_reset -port rst_n -phase neg -assert 0 -release 5逻辑说明第一条声明主时钟 clk周期 10ns占空比 50%。第二条声明第二个时钟域 ddr_clk周期 15ns并指定了相对主时钟的 2ns 偏移。-skew会让引擎在比对跨时钟域路径时留出时序余量如果没有这个参数SPV 可能会把两个时钟域相邻沿的逻辑路径当作同拍路径处理得出不真实的时序结论。参数说明-assert 0表示复位信号有效电平为 0-release 5表示在证明启动后第 5 拍释放复位让设计进入稳定初态。这条参数非常关键如果 release 设得太早设计还没完成初始化引擎会试图在未定状态上证明属性设得太晚等于强行走了一段人为延迟所有与复位相关的属性都会多出几拍的空窗。一般做法是先做一遍上电仿真数出从复位释放到所有状态机进入 IDLE 的实际拍数再把这个数填到 release 上。3.3 证明参数depth、engine 与并发数的隐藏关联很多新手拿到 SPV 后第一个动作是把证明命令抄过来直接跑结果跑十分钟没结果就认为是工具不行。实际上 SPV 证明任务的资源消耗和三个参数强相关扫描深度、引擎类型、并发进程数。三者互相制约。并发进程开得越多单个引擎分到的内存越少遇到大状态空间时反而容易提前内存耗尽。spv prove -scope a_fifo_prop -engine interp -depth 50 -mem 8g -jobs 4 spv prove -scope a_fifo_prop2 -engine ic3 -timeout 5400 -mem 16g -jobs 2逻辑说明第一行用插值引擎interp做深度 50 的有界证明分配 8GB 内存和 4 个并行进程第二行换成 IC3 无界证明超时时间设成 5400 秒内存翻倍但并发降到 2。原因在于 IC3 本身会维护大量子句多进程并发会导致内存快速分配反而降低单进程命中率。参数说明-depth 和 -timeout 在同一行出现时-timeout 会优先触发即到时间就停不管是否达到深度。如果希望证明必须在特定深度内完成就不要设 -timeout只保留 -depth反之想控制运行时长设 -timeout 会更容易预测回归任务的排期。-jobs 建议从两个维度考量跑批任务时按服务器物理核数的一半设跑单签核任务时直接设 1 到 2避免多个证明任务互相抢占缓存导致整体变慢。4. 把 SPV 放进 IC 验证流程与回归、覆盖率和门级网表协同4.1 formal 与 UVM 回归的分工formal 证明过的路径仿真不用再跑一个长期跑仿真回归的团队引入形式验证后最常见的困惑是两边都测同一个属性到底谁说了算我的处理原则很简单formal 负责证明仿真负责发现约束漏洞。formal 证明成功的属性同场景仿真回归可以直接摘掉因为数学上已经穷举formal 因为状态爆炸证不动的属性退回给仿真用定向用例覆盖。这种分工能让回归时间降一半前提是约束环境两边完全一致。# 从 SPV 导出仿真约束供 UVM sequence 复用 spv export_constraints -format uvmtpl -out sim_env/fifo_c_model_cons.sv # 回归脚本里跳过已证明的属性只跑未收敛项 spv regress -list formal_passed.lst -skip_success -mode regression逻辑说明第一行把 formal 验证环境里所有 assume 约束导出成 UVM 模板代码这个模板后续会被 sequence 组件直接实例化保证仿真里驱动的输入行为与 formal 环境一致。第二行是 SPV 自带的回归筛选读入已证明属性清单跑回归时自动跳过这些属性只检查尚未收敛的项。参数说明-format uvmtpl 导出的文件是片段不是完整组件需要手动包一层agent。有个坑导出的约束模板里如果有randomize with语句和 UVM 1.2 的std::randomize混用时可能冲突建议导出后先做一次静态检查。-skip_success依赖 SPV 的证明结果数据库如果之前用的不是寄存器式工程而是临时命令模式跑证明数据库是空的这个参数不会生效。4.2 功能覆盖率与 formal coverage两者刻度不一样别混着报IC verification 里覆盖率一直被当成进度条。但形式验证的 coverage 和仿真功能覆盖率是两个完全不同的东西。功能覆盖率统计的是“我测了哪些输入组合”formal coverage 统计的是“引擎在证明过程中到过哪些状态”。前者高说明用例写得多后者高说明证明的完备性好。SPV 里查覆盖率时要分清这两种输出别把 formal coverage 的百分比直接写进验证计划当功能覆盖率。指标仿真功能覆盖率SPV formal coverage统计对象输入组合与信号翻转状态点与分支路径驱动方式随机约束用例证明引擎自动搜索完备性含义只代表采样过的场景代表可达状态覆盖度不足时的处理增加用例或约束加深深度或放宽抽象签核参考价值中高要配合证明结果表格说明formal coverage 达到 95% 以上且证明通过这个数字在签核时比仿真功能覆盖率的 100% 更有说服力因为它意味着设计内部状态点在数学上被完整探索过。但反过来如果 formal coverage 只有 60%证明却通过了要警惕是不是约束过强把实际可达状态剪掉了。4.3 门级网表验证RTL 属性重跑要额外盯四件事RTL 上证完的属性到门级网表阶段不能直接复用原命令跑一遍就收工。网表里的逻辑结构变了时钟树插入、扫描链、DFT 逻辑都会影响证明结果。常见做法是单独建一个网表验证工程同一份断言文件重新读入但要做额外设置spv read_file -f netlist/fifo_top.gate.v spv read_file -f netlist/fifo_top_gateview.pkg.sv spv set_top -module fifo_top -view gate spv add_clock -port clk -period 10ns -tree enable spv add_reset -port rst_n -phase neg -assert 0 -release 3 spv prove -scope a_grant -engine ic3 -timeout 7200逻辑说明-view gate告诉 SPV 当前加载的是逻辑门级网表断言安装方式与 RTL 不同。-tree enable允许引擎自动追踪时钟树路径否则网表里插入的 buffer 链会让引擎把同一时钟当成两种不同信号。参数说明门级网表验证时RTL 里 5 拍就能收敛的属性常常要跑到 20 拍以上因为门延迟把逻辑深度撑大了。timeout 建议给足两小时以上。另一个容易翻车的是 DFT 信号网表里 scan_en 不能不加约束直接自由跑必须像复位一样用 constraint 固定为 0否则扫描链会把所有状态翻转一遍产生大量假反例。5. SPV 使用避坑从假失败到内存爆炸的五个真实案例5.1 反例跑到 DMA 模块输入约束没写全现象证明一个 FIFO 满标志属性SPV 返回的反例路径显示错误路径穿过 DMA 控制器驱动了一串完全不合理的总线请求最终把 FIFO 打满。原因只对 FIFO 的输入端口做了 basic 约束没有约束与之连接的总线控制器信号。引擎把总线控制器的输出当自由变量生成了正常芯片设计中永远不可能出现的激励。解决把与 FIFO 交互的上下游接口全部补上协议级 assume例如仲裁器在同一时刻只能发一个请求、DMA 传输长度不能超过最大阈值等约束。从那以后把所有与顶层端口直连的外设输入全部列入约束清单再跑证明。5.2 证明挂死存储阵列把状态空间撑爆现象证明一个带 8KB 配置存储的模块属性跑了 40 多分钟没有结果服务器内存直接飙到 32GB最后被 OOM killer 杀掉。原因引擎尝试枚举存储内所有配置值的组合存储字数的平方级状态让可达状态集合爆炸。解决把存储体替换成抽象模型——用黑盒代替存储阵列只保留读写端口和一个非确定性数据输出。在 SPV 里设置 cutpoint让引擎只验证控制逻辑不验证存储本身。存储内容的正确性交给后续内存内建自测试去覆盖。5.3 仿真过了 formal 挂了两态仿真的 X 态差异现象同一个属性在仿真的 20 万个用例里全部通过formal 环境里跑了不到一分钟就报反例。反例显示一个状态位在未知值 X 下进入了分支。原因RTL 仿真默认二值逻辑X 态传播不彻底formal 引擎默认对未初始化信号赋自由值会暴露二值仿真看不到的亚稳态路径。解决在复位约束里把所有内部状态寄存器的初值显式设置为 0而不是依赖引擎随机赋值。同时用-init_policy zero让所有状态位从确定初值开始。另外检查反例里的 X 态信号确认设计是否存在未初始化的同步逻辑。5.4 属性长时间不收敛触发太弱或时间窗过宽现象一条属性能在 30 拍内找到反例但想证明它无界时引擎连续跑了五个小时无结果。原因这条属性的触发条件是“任意请求到来时”这个条件太宽泛引擎无法在有限时间内剪掉无关状态。解决把属性分解成两条——一条只证“请求合法时响应必须发生”另一条证“请求非法时不能产生响应”。同时把时间窗从##[0:5]收紧到##[1:3]减小搜索空间。拆完之后两条属性都在 90 秒内收敛了。5.5 反例回放不回 RTL 仿真两边环境不一致现象formal 报了一个反例路径按时间线回放到 simulator 里仿真跑完全程没有冲突断言没有挂。原因formal 环境里设为 assume 的信号在仿真平台的 sequence 里没有被等效驱动两边输入环境的自由程度不同。formal 里能出现的激励序列仿真因为约束写得太严格而永远产生不了。解决把 formal 的约束原样导出成 UVM 约束模板替换掉仿真的手写 sequence。之后反例回放和 formal 结果完全一致。从那以后每次接 formal 反例第一件事就是检查约束导出清单而不是急着打开波形。6. 更进一步让 SPV 证明按时收敛的三个调试技巧6.1 用抽象替换存储体把设计里超过 4KB 的 RAM 全部标记为 cutpoint。具体做法是对存储输出设置抽象点让引擎只看到接口不展开内容。这会损失对存储数据正确性的验证但换来的是控制逻辑能在半小时内完成证明。存储正确性交给仿真定向用例去补。6.2 把复合属性拆成原子命题一条属性里同时带握手、计数、超时三个逻辑条件收敛难度呈指数上升。拆成三条原子属性分别验证后再用一条顶层属性把三者串起来。拆的时候注意保持原子属性之间的依赖关系清晰不要跨属性引用中间信号否则证明结果会互相干扰。6.3 用反例时序表判断问题归属SPV 每个反例都能导出成波形和时序表。我的习惯是先看信号变化列表不急着开波形窗口。如果反例在第三条约束处就出现自由变量非法翻转责任在约束环境如果所有约束都合法责任在设计逻辑。这个方法能把 70% 的假反例在第一分钟内定位掉。这些技巧单看都不难难的是每次证明任务都强制走一遍。尤其是抽象替换存储体这一步最容易因为“这次 RAM 不大、先放着”的想法跳过结果一跑就是几个小时后悔药都没处买。从那以后我每次搭验证工程都先做资源预算存储体超过 8KB 直接抽象属性超过三个逻辑条件强制拆分证明任务一律带上超时跑批。这套流程用下来SPV 的收敛成功率从刚开始的一半不到提升到了九成以上希望帮到你。本文还有配套的精品资源点击获取