第三章LPV 低功耗验证

概述

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

LPV Use Models

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

LPV 工作流程

加载 RTL 设计和 UPF/CPF 文件
构建 Power Model
运行结构检查
运行电源复位检查
验证电源属性

加载 Power File

# 加载 UPF 文件
load_upf -file design.upf

# 或加载 CPF 文件
load_cpf -file design.cpf

构建 Power Model

LPV App 自动从 UPF/CPF 构建设计的电源模型，包括：

电源域划分
电源开关（Power Switch）控制逻辑
隔离/保持/电平转换策略
电源状态表（Power State Table）

自动结构检查（Structural Checks）

自动验证以下结构要求：

所有关断域的输出都有隔离单元
不同电压域之间有电平转换器
需要保持的寄存器有 retention cell
电源开关的控制逻辑正确

# 运行结构检查
check_lpv -structural

电源复位检查（Power Reset Checks）

# 验证电源域关断/上电复位行为
check_lpv -power_reset

Power Properties Verification

自动生成和验证电源相关的断言：

域关断时输出被正确隔离
域上电后状态恢复正确
电源状态转换不会导致 X 传播

# 验证电源属性
check_lpv -properties

Auto-Assertions / Auto-Covers

LPV 自动生成断言和覆盖点：

Auto-Assertions：验证电源管理正确性
Auto-Covers：覆盖电源状态转换场景

# 证明自动生成的断言
prove -all

LPV 低功耗验证界面

LPV 低功耗验证界面 — 第 16 页截图

LPV 低功耗验证界面 — 第 29 页截图

LPV 低功耗验证界面 — 第 39 页截图

低功耗验证方法论

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

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

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

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

结构检查 vs 功能检查

类型	检查内容	特点
结构检查	隔离单元是否存在、连接是否正确、电源开关是否正确连接	静态分析，不需要证明引擎，快速
功能检查	隔离时序是否正确（关断前已隔离、打开前保持隔离）、保持寄存器 save/restore 行为	需要形式引擎证明，发现动态行为 bug

常见错误模式

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

来源文档

jaspergold_lpv_userguide.pdf
example_jaspergold_apps/LPV/