# 低功耗验证避坑指南：Formality+UPF自动化设置中电源网络处理的5个隐藏陷阱 在芯片设计的低功耗验证流程中，Formality与UPF（Unified Power Format）的结合使用，已经成为确保从RTL到门级网表功能等价性的标准操作。尤其是Automated Setup Mode（自动设置模式），它通过引入SVF（Synthesis Verification Format）文件，极大地简化了设置流程，减少了人为错误。然而，正是这种“自动化”带来的便利，往往让工程师放松警惕，忽略了底层电源网络处理的复杂性。电源网络并非简单的逻辑连接，它涉及到电源域（Power Domain）、隔离单元（Isolation Cell）、电平转换器（Level Shifter）以及保持寄存器（Retention Register）等一系列特殊单元。当技术库（.db文件）的电源引脚定义不完整，或者UPF描述与物理实现存在微妙差异时，Formality的自动设置可能会悄无声息地“通过”验证，但实际上埋下了功能错误的种子。这种“假验证通过”是低功耗设计验证中最危险的情况之一。 本文将深入剖析在Formality的Automated Setup Mode下，处理UPF电源网络时最容易踩中的五个隐藏陷阱。这些陷阱通常不会在常规的等价性检查中直接报错，而是通过一些变量的默认设置或特定场景下的行为，导致验证结果失真。我们的目标不仅仅是列出问题，更是通过实际的脚本片段、变量设置对比和调试思路，为你构建一套主动防御的验证策略。无论你是刚刚接触低功耗验证，还是已经在此领域深耕多年，希望这些从实际项目“踩坑”中总结的经验，能帮助你构建更健壮、更可信的验证流程。 ## 1. 陷阱一：`upf_use_additional_db_attributes`的默认真空与时钟门控单元“消失” `upf_use_additional_db_attributes` 这个变量是连接UPF意图与技术库物理属性的关键桥梁。在Automated Setup Mode下，它默认被设置为 `false`。这个默认值带来的第一个隐蔽问题，就是**时钟门控单元（Clock Gating Cell）和基于锁存的隔离单元可能被错误地忽略**。 **问题机理**：许多先进工艺库中的时钟门控单元或复杂的隔离单元，其内部包含时序元件（如锁存器）。UPF中的 `set_retention` 策略旨在控制保持寄存器的电源状态。当 `upf_use_additional_db_attributes` 为 `false` 时，Formality在遇到被标记为时钟门控或包含时序元件的单元时，会采取一种保守策略：它可能不会将这些单元视为受UPF策略控制的对象，或者直接将其从特定的电源网络分析中排除。更关键的是，对于技术库中定义为宏单元（`is_macro_cell : true`）的隔离器或电平转换器，其引脚上定义的 `related_power` 和 `related_ground` 属性会被完全忽略。 **后果**：这会导致验证模型与实际综合后网表的电源连接关系不一致。例如，一个本该由备用电源供电的隔离单元，在验证中被错误地关联到了主电源网络。由于逻辑功能可能暂时不受影响，验证会“通过”，但芯片在特定功耗模式下工作时，该隔离单元可能无法正确关断或隔离信号，导致功能失败或漏电。 **如何识别与规避**： 首先，你需要检查技术库文件。一个具备完整低功耗支持的技术库，其单元描述应包含明确的电源引脚（如`VDD`, `VSS`）以及相关的属性。 ```tcl # 示例：在Formality中报告某个单元的属性，检查是否有related_power/ground fm_shell> report_attribute -cell cg_latch_instance ``` 如果发现关键的低功耗单元缺少这些属性，或者你怀疑验证结果，应立即在设置SVF文件后，手动将 `upf_use_additional_db_attributes` 设置为 `true`。 ```tcl # 在read设计并load_upf之后，verify之前设置 set_svf default.svf # ... 读入reference和implementation设计 ... load_upf -r design.upf load_upf -i design_impl.upf # 关键：覆盖自动设置模式下的默认值 set_app_var upf_use_additional_db_attributes true ``` > 注意：将此变量设为 `true` 后，如果技术库单元（特别是寄存器）受 `set_retention` 控制但缺少DB模型，Formality会报错。这反而是件好事，它强迫你去检查和完善库模型，而不是掩盖问题。 为了更清晰地展示该变量设置前后对Formality行为的影响，可以参考下表： | 操作场景 | `upf_use_additional_db_attributes = false` (默认) | `upf_use_additional_db_attributes = true` (推荐) | | :--- | :--- | :--- | | **时钟门控/含时序元件的单元** | 可能被忽略，不参与特定UPF策略分析。 | 被正确识别，其电源连接受UPF策略影响。 | | **宏单元的`related_power/ground`属性** | 被忽略。在分析`set_isolation`的`-source/-sink`时可能使用错误电源。 | 被使用。用于确定隔离单元的源/漏电源，分析更精确。 | | **缺少DB模型的保留寄存器** | 发出警告，并将所有时序单元转换为保留单元（可能不准确）。 | 产生错误，阻止验证继续，要求提供准确模型。 | | **验证结果倾向** | 容易导致“假通过”，掩盖电源连接错误。 | 更严格，可能暴露库或UPF描述问题，导向“真失败”或“真通过”。 | ## 2. 陷阱二：`upf_assume_related_supply_default_primary` 的善意假设与端口电源歧义 当UPF描述或网表端口缺少显式的相关电源（related supply）定义时，Formality需要决定如何处理。`upf_assume_related_supply_default_primary` 变量控制着这一行为。在Automated Setup Mode下，它被设置为 `true`。 **问题机理**：这个设置的本意是“友好”的，它假设那些没有明确定义电源关系的端口，其驱动或接收电源默认为本地的主要电源（local primary supplies）。这听起来很合理，但在层次化设计或IP集成场景中，却可能引发严重问题。例如，一个子模块的输出端口，在顶层可能被连接到另一个电源域。如果该端口的UPF描述缺失或不够具体，Formality会基于这个假设，认为它仍然连接在原始电源域上，从而可能错过跨电源域的信号隔离或电平转换需求。 **后果**：验证会认为电源连接一致而通过，但实际物理连接是错误的。这可能导致信号在电源关断域中窜扰，或者电平不匹配，造成接收端电路误操作。 **如何识别与规避**： 首先，审查你的UPF文件，确保所有跨电源域接口的端口，都使用 `set_port_attributes` 或 `connect_supply_net` 等命令清晰地定义了电源关系。 对于关键设计，一个更安全的做法是**在初始验证时，将此变量设为 `false`**，让Formality对缺失电源定义的端口报错。 ```tcl # 在自动设置模式开启后，覆盖此变量 set_app_var synopsys_auto_setup true set_svf default.svf # 覆盖默认的“善意假设”，强制严格检查 set_app_var upf_assume_related_supply_default_primary false # 然后读入设计和UPF read_verilog -r top.v load_upf -r top.upf ... ``` 如果此时Formality报告大量关于端口电源定义的错误或警告，这正是你需要修复UPF描述的信号。在完善UPF后，你可以根据情况决定是否重新启用该假设以加速验证。一个折中的策略是，在项目早期和每次UPF有重大更新时使用 `false`，在后期稳定阶段使用 `true` 进行快速回归。 ## 3. 陷阱三：`verification_clock_gate_hold_mode` 与SVF中隐藏的时钟门控指令 时钟门控是低功耗设计的基础技术，但也是等价性验证的难点。Automated Setup Mode的一个优势是能自动处理时钟门控，其核心是 `verification_clock_gate_hold_mode` 变量。这个变量的值**并非直接由`synopsys_auto_setup`设置，而是由SVF文件中的 `guide_environment {{ clock_gating ... }}` 指令传递**。 **问题机理**：如果综合时使用的时钟门控策略（例如，是采用基于锁存器的门控还是组合逻辑门控）与Formality验证时采用的识别模式不匹配，就会导致时钟路径比较点无法匹配或验证失败。更隐蔽的是，如果SVF文件中没有包含 `guide_environment` 指令，或者指令中的模式（`...`）设置不当，`verification_clock_gate_hold_mode` 将保持其默认值 `none`。在 `none` 模式下，Formality不应用特定的时钟门控识别算法，很可能无法正确匹配被门控的时钟网络。 **后果**：大量与时钟门控单元相关的寄存器比较点匹配失败，验证报告出现大量“Unmatched”点。或者更糟，某些比较点被强制匹配，但由于时钟行为分析错误，导致功能等价性判断失误。 **如何识别与规避**： 1. **检查SVF内容**：使用Design Compiler命令生成SVF的明文版本，或查看Formality工作目录下的 `formality_svf/svf.txt` 文件，搜索 `guide_environment {{ clock_gating` 关键字。 ```tcl # 在DC中生成明文SVF参考（非必须，但有助于调试） # set_svf -verbose -output svf_verbose.svf ``` 2. **验证模式设置**：在Formality中，使用 `report_variables` 命令或在setup模式下查询该变量值。 ```tcl fm_shell (setup)> get_app_var verification_clock_gate_hold_mode ``` 3. **手动干预**：如果确认模式不正确或缺失，应在Formality脚本中手动设置。通常，对于常见的锁存器型时钟门控，设置为 `low` 是安全的起点。 ```tcl # 在set_svf之后，verify之前手动设置 set_app_var verification_clock_gate_hold_mode low ``` 如果设计中同时存在多种门控类型，或者时钟门控信号还驱动了输出端口，可能需要尝试 `any` 或 `collapse_all_cg_cells` 模式。 > 提示：不要完全依赖自动设置。在首次验证新设计或更换工艺库后，花时间确认时钟门控的处理方式是否正确，是避免后期调试痛苦的关键一步。 ## 4. 陷阱四：未驱动信号（Undriven Signals）处理模式与电源网络初始状态 `verification_set_undriven_signals` 变量决定了Formality如何处理参考设计和实现设计中未连接的信号。在Automated Setup Mode下，此变量被设置为 `SYNTHESIS`。这个设置旨在让Formality的行为与Design Compiler综合时的行为保持一致，初衷是好的，但在低功耗上下文中可能引入风险。 **问题机理**：在低功耗设计中，许多信号在电源关断后处于未驱动或未知（X）状态。`SYNTHESIS` 模式意味着，对于参考设计（通常是RTL），未驱动信号按DC综合的方式处理（通常更乐观，可能视为无关项）；对于实现设计（网表），则视为Cut-Net（逻辑锥的切割点）。如果电源控制逻辑本身存在缺陷，导致某些本应被驱动的信号在特定模式下悬空，这种处理差异可能会掩盖问题。例如，一个隔离单元的输出使能信号未正确驱动，在 `SYNTHESIS` 模式下可能被“宽容”处理，验证通过，但实际电路该隔离器可能永远不工作。 **后果**：验证通过，但芯片在功耗模式切换时，由于控制信号未驱动，导致隔离失效、保持状态丢失等严重功能错误。 **如何识别与规避**： 对于低功耗验证，一个更严格、更保守的策略是将此变量设置为 `BINARY:X`（这也是非自动模式下的默认值）。这样，参考设计中的未驱动信号被视为Cut-Net，实现设计中的视为X。如果任何参考设计中的比较点由未驱动信号控制，验证就会失败，从而暴露出潜在的控制逻辑缺陷。 ```tcl # 采用更保守的未驱动信号处理策略 set_app_var verification_set_undriven_signals BINARY:X ``` 在验证后期，为了追求验证通过率，你可能会放松此设置。但**强烈建议在项目初期和功能验证阶段使用 `BINARY:X`**，将其作为发现电源控制逻辑漏洞的“探针”。 此外，结合使用 `report_undriven_signals` 命令，主动列出设计中的所有未驱动点，逐一审查其合理性，是一个非常好的工程实践。 ```tcl fm_shell> report_undriven_signals -verbose ``` ## 5. 陷阱五：黑盒（Black Box）与层次化边界的电源感知缺失 在层次化验证或使用第三方IP时，黑盒处理是常态。Automated Setup Mode虽然简化了设置，但对于黑盒的电源感知处理，依然需要工程师额外关注。 **问题机理**：Formality要求参考设计和实现设计两边的黑盒模块必须匹配。但是，匹配不仅仅是模块名和端口名，还包括**端口的电源属性**。如果黑盒模块的端口没有在UPF中定义相关的电源网络，或者两边的定义不一致，Formality可能因为 `upf_assume_related_supply_default_primary` 的假设而静默通过，也可能在后续验证中引发难以追踪的失败。 **后果**：跨黑盒边界的信号可能被错误地关联到默认电源域，导致电平转换或隔离策略在该边界失效。由于黑盒内部逻辑不可见，这种错误在等价性验证中极难被发现，通常要等到系统级仿真或流片后测试才会暴露。 **如何识别与规避**： 1. **为黑盒创建精确定义的UPF模型**：即使不知道黑盒内部实现，也必须为其输入/输出端口定义清晰的电源属性。使用 `set_port_attributes` 命令。 ```tcl # 在UPF文件中为黑盒IP的端口定义电源属性 set_port_attributes -class port \ -ports {IP_block/A_in IP_block/B_in} \ -related_supply {PD_TOP/primary} set_port_attributes -class port \ -ports {IP_block/Z_out} \ -related_supply {PD_IP/primary} ``` 2. **在Formality中显式设置黑盒匹配**：使用 `set_black_box` 命令，并确保两边的黑盒实例都被正确设置。同时，可以利用 `set_user_match` 命令，手动匹配黑盒两侧的端口，特别是当端口名因层次化而改变时。 ```tcl fm_shell (setup)> set_black_box r:/WORK/top/analog_ip fm_shell (setup)> set_black_box i:/WORK/top/analog_ip # 如果端口名不同，手动匹配 fm_shell (setup)> set_user_match r:/WORK/top/analog_ip/clk i:/WORK/top/analog_ip/CLK_I ``` 3. **进行层次化验证（Hierarchical Verification）**：对于大型设计，将黑盒所在模块单独拎出来进行验证，可以缩小问题范围。使用 `write_hierarchical_verification_script` 命令生成脚本。 ```tcl set_top i:/WORK/top write_hier -replace -level 2 hier_verify.tcl # 然后检查生成的脚本，确保黑盒和电源设置被正确继承。 ``` **构建一个防御性的验证脚本模板**： 最后，结合以上所有要点，一个健壮的、能主动规避陷阱的低功耗Formality验证脚本框架应如下所示： ```tcl # 低功耗验证防御性脚本框架 set_app_var synopsys_auto_setup true # 陷阱1 & 2: 覆盖关键UPF变量默认值，转向严格模式 set_app_var upf_use_additional_db_attributes true set_app_var upf_assume_related_supply_default_primary false set_svf default.svf # 陷阱3: 根据设计手动确认或设置时钟门控模式 # set_app_var verification_clock_gate_hold_mode low # 读入参考设计 read_db -r tech_lib.db read_verilog -r top.v sub1.v sub2.v set_top r:/WORK/top load_upf -r top.upf # 读入实现设计 read_db -i tech_lib.db read_verilog -i top_impl.v set_top -auto load_upf -i top_impl.upf # 陷阱4: 采用保守的未驱动信号处理策略 set_app_var verification_set_undriven_signals BINARY:X # 陷阱5: 显式处理黑盒 set_black_box r:/WORK/top/blackbox_inst set_black_box i:/WORK/top/blackbox_inst # 可选：报告未驱动信号以供审查 report_undriven_signals -out undriven.rpt # 执行验证 verify ``` 在实际项目中，我多次遇到因为迷信“自动通过”而险些漏掉重大电源连接错误的情况。最深刻的一次教训是，一个时钟门控单元因为库属性缺失，在验证中被完全忽略，导致其所在电源域的状态保持功能失效，这个问题直到功耗仿真阶段才偶然发现。从那以后，我养成了在每次低功耗验证项目启动时，首先检查并手动设置 `upf_use_additional_db_attributes` 和 `verification_set_undriven_signals` 的习惯。把Formality的自动模式看作一个强大的助手，而非全自动的黑箱，用明确的变量设置和审查流程为你的验证结果加上“保险”，这才是通往一次流片成功更可靠的道路。