第三章LPV 低功耗验证

概述

低功耗验证App 验证 UPF（Unified Power Format）文件所描述的电源管理行为是否被正确实现。

电源格式说明：平台用户指南在 LPV App 一节写明该 App「supports the standard UPF and CPF power intent specification formats」（jaspergold_apps_userguide.pdf 第 36 页）。不过 LPV 专用用户指南与命令参考中只有 UPF 流程——加载命令是 check_lpv -load_upf，支持 -upf_version 取值 1.0、2.0、2.1，文档并明确指出 JasperGold Apps 不支持 UPF 3.0。本章后续内容因此全部按 UPF 讲解；CPF 在这套文档里没有对应的加载命令或示例。

LPV Use Models

验证电源域（Power Domain）切换行为
验证隔离单元（Isolation Cell）插入正确
验证保持寄存器（Retention Register）行为
验证电平转换器（Level Shifter）
验证电源状态转换

LPV 工作流程

加载 RTL 设计和 UPF 文件
生成电源设计（Power Design）
运行各项结构检查
创建并证明电源断言/覆盖点

加载 UPF 并生成 Power Design

这是驱动整个 LPV 流程的两条核心命令：

# 加载 UPF 文件
check_lpv -load_upf top.upf

# 生成电源设计
check_lpv -generate_power_design

-load_upf 的可选项包括 -upf_version (1.0 | 2.0 | 2.1)、-scope instance_path、-allow_unescaped_bus_index。

构建 Power Model

UPF 所描述的电源意图（power intent），按文档定义包含以下内容：

电源域与电压域（power and voltage domain）
供电网络（supply network）——其中 supply net 是用于连接域与设计中各组件电源引脚的内部网线，supply port 则是为器件提供电压供应的外部端口
电源开关（power switches）
隔离单元与电平转换器（isolation cells and level shifters）
保持单元（retention cells）
电源状态/模式（power states/modes）
电源状态表（power state table）——定义合法的配置组合

几个容易混淆的相关术语：

Power state（电源状态）：设计的一个稳态，其中部分电源域开启、部分关闭。
Power sequence（电源序列）：由一系列状态转换构成的下电与上电状态序列，其中每个给定状态控制一个具体的电源组件，例如门控时钟、隔离和保持。
State retention cells（状态保持单元）：帮助已下电的块恢复正常工作；可用于部分时序单元，使其在下电前保留原有状态。
Save/restore 控制信号：当 save 控制引脚被激活且电源处于开启状态时保存当前值，当 restore 控制引脚被激活时恢复所保存的值。

结构检查（Structural Checks）

结构检查不是一条笼统的命令，而是通过 check_lpv -verify <检查名> 逐项运行的。官方示例中的完整序列：

check_lpv -verify check_iso_clk_all
check_lpv -verify check_iso_inputs
check_lpv -verify check_iso_outputs
check_lpv -verify check_iso_ctrl_rst
check_lpv -verify check_iso_connections
check_lpv -verify check_ret_connections
check_lpv -verify check_iso_default_value
check_lpv -verify check_ret_ctrl_rst
check_lpv -verify check_power_switch_connections
check_lpv -verify check_power_switch_ctrl_rst

几项典型检查的含义：

check_iso_outputs：检查电源域边界实例的输出
check_ret_connections：检查保持（retention）规则的 power net、save/restore 信号和保持元件不为空
名称中带 _ctrl_rst 的几项即电源复位相关检查（隔离、保持、电源开关的控制复位）

电平转换器（level shifter）的价值在于：文档指出只有结构验证才能发现某些错误，例如缺失的电平转换器。

Auto-Assertions / Auto-Covers

断言和覆盖点用 check_lpv -create <名称> 创建。官方示例中的序列：

# 隔离相关断言
check_lpv -create assert_iso_up_before
check_lpv -create assert_iso_supply
check_lpv -create assert_iso_up_after
check_lpv -create assert_iso_up_clk_stable
check_lpv -create assert_iso_change_signal_stable

# 保持（retention）相关断言
check_lpv -create assert_clock_stable_after_restore
check_lpv -create assert_ret_supply_on_save
check_lpv -create assert_ret_supply_on_restore
check_lpv -create assert_ret_supply_on_from_save_to_restore

# 覆盖点
check_lpv -create cover_power_switch_ctrl
check_lpv -create cover_iso_ctrl
check_lpv -create cover_ret_save_ctrl

# 证明
prove -all

其他可创建的项还包括 assert_all、cover_all、cover_pst_states、assert_supply_onehot、assert_ret_no_save_on_restore、assert_pd_supply_change_clk_stable、assert_rst_non_ret_flops 等。

LPV 低功耗验证界面

低功耗验证方法论

为什么低功耗需要形式验证

低功耗设计使用 UPF（Unified Power Format）描述电源意图：哪些域可以关断、隔离单元的位置、保持寄存器的策略。UPF 相关 bug 包括：

隔离单元漏插——关断域的输出在关断时传播 X 到常开域
隔离值错误——应该隔离为 0 但隔离为 1（或反之）
隔离控制信号时序错误——电源关断前隔离未使能、电源打开前隔离过早释放
保持寄存器 save/restore 时序错误——数据在电源关断前未保存或恢复时数据丢失
电源开关连接错误

这些 bug 在仿真中很难触发（需要精确的电源状态转换序列），但形式验证可以穷举所有电源状态转换来检查。

三类验证的能力边界

LPV 的验证分为结构（Structural）、电源复位（Power Reset）、电源属性（Power Properties）三类。文档强调的重点不是"哪类更强"，而是三者各有独占的发现能力，必须配合使用：

类型	文档给出的能力边界
三类验证都能发现许多低功耗错误，例如缺失的隔离单元（missing isolation cell）
结构验证	只有结构验证能发现某些错误，例如缺失的电平转换器（missing level shifter）
电源复位验证 / 电源属性验证	只有这两类能发现另一些错误。文档给出的例子：结构检查无法发现"隔离钳位为高而非为低"，但电源复位验证可以

LPV App 会根据设计结构与行为、电源意图（power intent）和低功耗设计准则，自动创建 power-aware RTL 和一组检查；随后由 JasperGold 的穷尽证明技术针对所有可能的输入组合评估这些低功耗检查，以确认 DUV 的完整性。

常见错误模式

assert_iso_up_before 失败 → 隔离使能晚于电源关断，关断时输出未隔离
assert_ret_supply_on_save 失败 → save 操作时保持寄存器的电源不正确，数据丢失
cover_power_switch_ctrl 不可达 → 电源开关控制信号被约束阻塞，状态转换无法发生

来源文档

jaspergold_lpv_userguide.pdf
example_jaspergold_apps/LPV/