第1章 低功耗设计与UPF基础：核心概念、原理机制、实战要点
1.1 问题背景：功耗复杂度挑战验证
在先进工艺节点，功耗已成为芯片竞争力的核心指标。动态功耗与电压平方成正比，静态漏电功耗随尺寸缩小呈指数增长。多电压域、电源门控、DVFS等低功耗措施在降低功耗的同时，也引入了大量“仅在特定电源状态下有效”的电路行为。
- 动态功耗：α·C·V²·f
- 静态功耗：V·Ileak
传统仿真验证难以穷举所有电源状态组合，低功耗缺陷可能在特定状态下才出现，导致芯片“唤醒即死”或“休眠数据丢失”。
1.2 核心概念：UPF与形式化验证
UPF（Unified Power Format，IEEE 1801）是描述低功耗设计意图的标准格式。它将“什么时候关电、什么时候隔离、哪个域必须保持”等策略，形式化地表达为设计的一部分。形式化验证则通过数学证明，系统性地检查这些策略在逻辑上是否正确。
每个环节做什么？
- RTL设计：在RTL阶段加入低功耗单元和时钟门控。
- UPF功耗意图：用IEEE 1801命令描述电源域和状态。
- 形式化建模：将UPF和网表转为形式化模型。
- 属性检查：证明隔离、保持、电平转换等属性。
- 签核收敛：修复问题并完成低功耗签核。
1.3 原理机制：从功耗意图到验证属性
UPF通过一组命令定义电源网络和状态：
create_power_domain PD_TOP
create_supply_port VDD
create_supply_port VSS
create_supply_net VDDN -domain PD_TOP
create_supply_net VSSN -domain PD_TOP
connect_supply_net VDDN -ports VDD
connect_supply_net VSSN -ports VSS
set_domain_supply_net PD_TOP -primary_power_net VDDN -primary_ground_net VSSN当UPF描述完成后，形式化验证工具提取以下关键信息：
- 电源域边界：哪些单元归属于哪些域。
- 电源状态表：不同状态下各域电压/关断情况。
- 隔离策略：信号穿越关断域时如何处理。
- 保持策略：寄存器是否需要在断电后保存原值。
1.4 流程步骤：五步完成UPF形式化验证
- 输入准备：核对RTL网表、UPF文件、库单元属性。
- 环境配置：指定电源状态和库单元信息。
- 模型建立：生成形式化模型，包括状态机和非确定性选择。
- 检查执行：运行隔离、保持、电平转换、电源域连接等检查。
- 结果分析：分析反例，修复UPF或RTL，回归收敛。
提示：不要等到流片前才做UPF验证。建议在RTL freeze前开始，每次UPF改动后都跑一轮形式化检查，成本远低于功能仿真。
1.5 案例说明：CPU域关闭时的隔离验证
某SoC中包含CPU域（可关断）、GPU域（可关断）和Always-On域。当CPU域关闭时，CPU域输出信号必须被隔离单元钳位到固定值，否则下游常开域会看到X态。
UPF中定义了隔离单元和策略：
set_isolation iso_cpu -domain PD_CPU
set_isolation_control iso_cpu -isolation_sense high
set_isolation_value iso_cpu -value 0形式化验证需要证明的属性是：CPU_OFF -> ISO_ENABLE == 1。工具会遍历所有可能到达CPU_OFF的路径，检查是否存在使能信号的缺口。如果发现反例，说明存在一个唤醒/关闭序列会使隔离单元失效。
1.6 表格总结：低功耗设计与UPF关键概念
| 概念 | 说明 | 验证关注点 |
|---|---|---|
| 电源域 | 由同一电源状态控制的逻辑集合 | 域边界完整、无漂移信号 |
| 电源状态 | 电压或关断的组合状态 | 合法状态、切换路径 |
| 隔离单元 | 关断域输出钳位到指定值 | 隔离使能、钳位值 |
| 电平转换器 | 跨电压域信号的电平适配 | 方向、电压组合 |
| 保持单元 | 断电时保存寄存器状态 | 保存/恢复控制时序 ← 上一章 📖 返回目录 下一章 → |