Formality验证总失败？先别急着改设计，试试这个变量：verification_set_undriven_signals

Formality验证失败排查指南：verification_set_undriven_signals的实战应用

当Synopsys Formality报告验证失败时，许多工程师的第一反应是检查RTL设计是否存在逻辑错误。但经验丰富的验证工程师会告诉你：先别急着改代码。在最近的项目中，我们团队遇到一个典型案例——Formality连续三次验证失败，最终发现80%的失败点都是由未驱动信号（undriven signals）引起，而调整verification_set_undriven_signals变量后问题迎刃而解。这个变量就像Formality的"敏感度调节器"，理解它的工作原理能帮你节省大量无效调试时间。

1. 未驱动信号为何成为验证"拦路虎"

在数字电路设计中，未驱动信号指的是那些没有被任何驱动源（如寄存器输出、模块端口或常量赋值）直接驱动的网络或引脚。它们就像城市中失去GPS信号的车辆，行为不可预测。Formality对这类信号的处理策略直接影响验证结果。

典型场景举例：

• 模块的输入端口在测试环境中未被连接
• 设计中被注释掉的功能模块遗留的中间信号
• 条件生成语句（generate if）中未被选中的分支信号

# 查看未驱动信号的Formality命令 report_undriven_nets -all report_undriven_pins -all

当这些"游离"信号影响到比较点（compare points）时，Formality的默认保守策略会直接判定验证失败。这其实是个安全机制——宁可误报也不漏报，确保设计中没有意外依赖未驱动信号的情况。

2. verification_set_undriven_signals的六种武器

这个变量的配置本质上是告诉Formality："当遇到未驱动信号时，请按照以下方式处理"。其可选值构成一个从严格到宽松的频谱：

关键选择逻辑：

if (确认未驱动信号是设计意图) { set_app_var verification_set_undriven_signals 0; # 或1/X/Z } else { set_app_var verification_set_undriven_signals BINARY:X; }

3. 调试工作流的黄金四步法

基于多个Tape-out项目的经验，我们总结出以下高效排查流程：

1. 定位元凶
   首先运行失败分析命令，确认未驱动信号是否参与失败路径：

   analyze_failures -verbose report_failing_points -nosplit

2. 评估影响范围
   使用以下命令统计未驱动信号数量及其层级分布：

   report_undriven -summary -hierarchical

3. 策略选择矩阵
   根据信号性质决定处理方式：

   信号类型	推荐配置	后续动作
   设计疏忽导致的悬空信号	BINARY:X	返回RTL修正
   故意保留的测试信号	0/X/Z	添加注释说明
   条件化功能模块接口	BINARY	检查generate条件覆盖
   跨时钟域隔离信号	同步策略后验证	确保同步器结构匹配

4. 渐进式验证
   对大型设计建议分阶段验证：

   # 第一阶段：快速筛查 set_app_var verification_set_undriven_signals 0 verify # 第二阶段：精确分析 if {[get_failing_points -count] > 0} { set_app_var verification_set_undriven_signals BINARY:X verify }

## 4. 高级应用：与综合工具的协同策略 当使用Design Compiler进行综合时，其默认会将未驱动信号接地（tie to 0）。这可能导致Formality验证时的参考设计和实现设计行为不一致。此时需要特殊处理： **典型协同配置方案**： ```tcl # 保持与DC一致的处理方式 set_app_var synopsys_auto_setup true set_app_var verification_set_undriven_signals SYNTHESIS # 或者显式指定接地策略 set_app_var verification_set_undriven_signals 0:X

特别注意：在先进工艺节点（如7nm以下）设计中，未驱动信号可能引发静电放电（ESD）风险。我们建议即使验证通过，也应在物理实现阶段通过UPF（Unified Power Format）约束明确处理所有未驱动信号。

5. 实战中的"坑"与应对技巧

在一次PCIe 5.0控制器的验证中，我们发现一个诡异现象：相同RTL在不同机器上的Formality运行结果不一致。根本原因是团队成员的脚本中混用了两种设置方式：

# 错误示例：两种设置方式混用 set verification_set_undriven_signals 0 set_app_var verification_set_undriven_signals BINARY:X

最佳实践：

• 统一使用set_app_var语法
• 在脚本开头显式设置变量
• 添加注释说明配置理由
• 对关键配置进行assert检查：

  if {[get_app_var verification_set_undriven_signals] ne "BINARY:X"} { puts "WARNING: 非常规未驱动信号设置!" }

另一个常见问题是ECO阶段忽略未驱动信号处理。某次28nm项目在功能ECO后Formality突然失败，最终发现是新增的tie-cell使原先的未驱动信号现在被显式驱动，而验证环境未同步更新。这时需要重新评估verification_set_undriven_signals的配置合理性。