UPF电源意图建模：核心概念、原理机制、实战要点
低功耗设计已经从“单一电源域＋全局时钟门控”发展为多电压域、动态电源门控、多阈值单元并存的新架构。RTL 只描述逻辑功能，无法回答“某个模块何时允许断电”“跨域信号是否被隔离”“寄存器数据在掉电时是否必须保留”等问题。UPF（Unified Power Format）是 IEEE 1801 标准定义的电源意图描述语言，为逻辑网表之外建立一套可读、可仿真、可验证的电源规格。
问题背景：形式化验证为什么要先谈电源意图建模
形式化验证通过穷举状态空间来证明属性。如果输入模型没有电源行为约束，工具会把“断电状态”当作普通状态处理，导致大量伪错误或严重漏检。UPF 建模的核心目标，就是为形式化引擎提供一张“电源世界的真值表”，使工具明确知道：什么条件下信号有效、单元可被关闭、数据必须保留。
UPF 电源意图建模相当于给形式化验证提供一份“电源行为契约”。这张契约不完整，验证结果就不可信。
核心概念：UPF 如何表达电源意图
UPF 将“电源意图”分解为可识别、可校验的元素：电源域描述逻辑归属，供电集合描述实际电压轨，电源状态描述可用电压排列，低功耗策略描述隔离、电平转换和数据保持要求。四者共同构成一张完整的电源意图网络。
图：UPF 电源意图建模核心要素
核心概念速查表
| 概念 | 缩写 | 作用 | 形式化验证意义 |
|---|---|---|---|
| 电源域 | Power Domain / PD | 将逻辑单元划分到同一供电控制的区域 | 界定上电/掉电范围，验证域间隔离 |
| 供电集合 | Supply Set / SS | 描述一组电压轨（power/ground） | 追踪电压源连接，检查供电缺失 |
| 电源状态 | Power State | 描述各域可组合的供电状态 | 驱动 P S T，验证合法状态迁移 |
| 隔离策略 | Isolation | 在断电域输出端加入钳位逻辑 | 验证隔离使能条件与输出值 |
| 电平转换器 | Level Shifter | 匹配跨域信号电压范围 | 检查缺失、重复或方向错误 |
| 数据保持 | Retention | 掉电时保存关键寄存器状态 | 验证保存/恢复时序 |
原理机制：UPF 定义如何被形式化验证消费
UPF 命令本身是 Tcl 风格文本，例如 create_power_domain。形式化验证工具读入 UPF 后，先解析命令、构建电源意图模型，再把它映射为信号约束、单元属性和状态转换条件。其中最关键的是“电源状态表（PST）”：它列出了各电源域允许的电压组合、状态名和恢复顺序。验证引擎根据 PST 生成状态机约束，从而证明 UPF 与实际逻辑网表的行为一致。
关键命令包括但不限于：
create_power_domain：划分电源域；create_supply_set：定义供电集合；add_power_state：补充电源状态；set_isolation/set_level_shifter/set_retention：定义跨域策略。
典型建模流程
- 收集各模块供电需求，明确哪些模块常开、哪些可关闭；
- 用
create_power_domain创建电源域，包含域内逻辑； - 用
create_supply_set为每个域定义/绑定供电集合； - 用
add_power_state建立电源状态表和合法迁移条件； - 用
set_isolation、set_level_shifter、set_retention声明跨域策略； - 输出 UPF 文件，交给形式化验证工具做一致性、连通性和时序属性检查。
案例说明：双电源域 UPF 建模片段
假设一个 SoC 包含常开 IO 域和可关断 Core 域。RTL 顶层为 rtl_top，下面给出最小 UPF 建模片段：
set_scope rtl_top
# 创建电源域
create_power_domain PD_CORE -include_scope ./*
create_power_domain PD_IO
# 创建供电端口和供电集合
create_supply_port VDD_CORE
create_supply_port VDD_IO
create_supply_set ss_core -function {power VDD_CORE}
create_supply_set ss_io -function {power VDD_IO}
# 隔离 Core 域输出
set_isolation iso_core -domain PD_CORE \
-isolation_power_net VDD_IO \
-isolation_control signal
在形式化验证中，上述 UPF 会被解释为：当 signal 有效且 PD_CORE 掉电时，PD_CORE 输出必须钳位到 VDD_IO 对应的逻辑值。如果钳位值缺失或时序错误，工具将报告反例。
表格总结：UPF 建模元素与验证检查项
| 建模元素 | UPF 命令 | 常见验证检查项 |
|---|---|---|
| 电源域 | create_power_domain | 域边界完整，无未划分逻辑 |
| 供电集合 | create_supply_set | 电源端口连接完整，无浮空 |
| 电源状态 | add_power_state | 状态组合合法，迁移可达 |
| 隔离 | set_isolation | 隔离使能信号与电源状态同步 |
| 电平转换 | set_level_shifter | 所有跨电压域信号都有转换 |
| 数据保持 | set_retention | 保持信号在掉电前建立，恢复后释放 |
常见误区提醒
- 把 UPF 当成仿真注释，不参与形式化验证，导致电源关系完全漏检；
- 只定义电源域，不定义供电集合和 PST，状态机缺少底层数据；
- 隔离策略的钳位值没有指定或未连接“隔离供电电源”；
- 多份 UPF 合入时重复定义，默认规则被错误覆盖；
- 忽略断电域与常开域之间的时钟/复位交叉，跨域路径未加隔离。
工程实践清单
- 在 RTL freeze 前完成 UPF 基线，并在每个迭代版本运行形式化检查；
- 验证每个电源域都有明确的常开/可关断属性和 PST 条目；
- 检查所有跨域信号，确保已有隔离或电平转换策略；
- 对 PST 做覆盖率检查，确保所有手动声明状态都被使用；
- 将 UPF 和 RTL/门级网表一起纳入版本控制，保证验证结果可复现。