极客工场

Appearance

共 2,705 字预计阅读约 9 分钟

Formality 引用无法解析：link 后 Unresolved references 与黑盒速查 ​

更新时间：2026-10-22。FAQ 速查页，属于 EDA 工具排错系列，总入口见 EDA 开源与报错索引。Formality（fm_shell，Synopsys 形式验证工具）把参考侧 RTL 与实现侧网表读进 r/i 两个容器后，要先 link 出完整层次才能 match、verify。「引用无法解析」就发生在这一步：某个模块例化了一个名字，但容器里没有任何定义能接住它。它和读入阶段的「找不到文件」是两回事——后者断在 read_verilog，本篇断在 link 之后、以悬空引用和黑盒的形态出现，处置不当会把错误推迟到 match 甚至制造假不等价。读入阶段的问题见 Formality 模块/单元找不到，外部依赖视角见 Formality 依赖缺失，完整流程见 形式验证（二）：LEC/Formality。

本文要回答的问题 ​

  • link 后报 Warning: ... has N unresolved references，这些引用是怎么悬空的，为什么读入阶段不报错？
  • report_unresolved_references 的输出该怎么看，怎样从一个悬空名反推缺的是什么？
  • parameter 生成的条件例化、uselib、case 配置 define 在什么情况下会让引用在某一侧凭空消失？
  • 网表里工艺库单元名解析不了，为什么补 RTL 文件没用？
  • hdlin_unresolved_modules = black_box 为什么是最危险的一个变量？

一、报错原文与现象 ​

引用悬空在三个时点冒头：set_top 触发链接时、显式 link 之后、以及进入 match 时以黑盒/未映射比较点的形态爆发。典型形态如下。

形态一，link 汇总警告与逐条悬空名：

text
Warning: Design 'top' has 2 unresolved references in the
         reference container during link.
Warning: Unresolved reference 'fifo_async' in design 'dma_core'.
Warning: Unresolved reference 'SDFFRX4' in design 'top'.

形态二，implemented 容器里出现黑盒，以及两侧黑盒不对称：

text
Warning: 1 black box exists in the implementation container:
         'rm_sram_2k'.
Information: 15 compare points are unmapped (first: UID_318).
Warning: Reference-only modules: 2; Implementation-only modules: 0.

形态三，读入时没有任何 Warning，问题被变量静默放过：

text
Information: Unresolved module 'arbiter_dyn' treated as black box
             ('hdlin_unresolved_modules' = black_box).

判读口径：引用名全大写或形如 SDFFRX4、RM_1Kx32 的，是工艺库单元或硬 IP，缺的是库；全小写的 RTL 模块名，缺的是设计文件或配置。关键认知是：这些信息在默认日志里大多只是 Warning，Formality 不会因此中止。悬空引用被挂成黑盒后流程照跑，直到 match 阶段两侧锥结构对不上，才以 UID_数字 未映射点集中爆发；verify 即使跑完，结论也不覆盖这些锥。

二、报错 → 原因 → 处置速查表 ​

悬空引用/现象最可能原因一条命令确认处置
小写 RTL 模块名（reference 侧）filelist 漏文件、package 未先读report_unresolved_references -r补文件，按 package→子模块→顶层重读
小写 RTL 模块名（两侧同时）uselib 指向的库目录缺失查 RTL 中 uselib dir=...补 search_path 或改为显式 filelist
parameter 生成的例化名条件例化在该参数配置下不存在对两侧 report_parameter对齐两侧参数，属配置差异则设 dont_verify
全大写单元名（网表侧）工艺库 .db 未读或工艺角不匹配list_libs、get_cells -hier *SDFFR*read_db 补同工艺角库
老库单元名/库外单元网表用了旧库或非本工艺单元grep 网表单元名与 .db 对拍用同次综合的库，禁止随便找 .v 顶替
define 控制的例化r/i 两侧宏开关不一致对比读入命令 -define 集合由单一 filelist 驱动，宏集合对齐
层次名/大小写不符Linux 大小写敏感、转义名差异report_design -r/-i 对清单按真实名修正 filelist 与 set_top
SV interface/package 引用包未先读或实例化方式两侧不一致查报错符号是否为类型名package 先 analyze，两侧同语言标准
读入无 Warning 却有黑盒hdlin_unresolved_modules=black_boxreport_black_box -r/-i显式设为 error，清单外黑盒回查

三、排查决策树 ​

看到未解析引用，先给悬空名定性，再决定补文件、补库还是对配置，顺序不要反：

eda/ts-formality-unresolved-reference.md D2 示意图

读图抓住一条主线：红色入口之后，蓝色两步先把悬空名从报告里捞出来、再按命名形态分流——全小写走橙色「补设计」通道（文件、uselib、宏），全大写或硬 IP 名走「补库」通道，条件例化与静默黑盒走「对配置」通道；三条修复路汇合到绿色终点，未解析引用不归零就不进入 match。颜色只表达角色：红=现象，蓝=排查，橙=修复，绿=通过标准。

四、逐条排查展开 ​

1. 先用 report_unresolved_references 让悬空引用全部交代。 link 的汇总行只给数量，真正干活的是逐条报告：

tcl
set_top r:/work/top
set_top i:/work/top
report_unresolved_references -r
report_unresolved_references -i
report_black_box -r
report_black_box -i

输出按「父设计 → 悬空名」组织，先看引用出现在哪个父模块，再 grep 该父模块的例化语句，就能确认这个名字在 RTL 里是以什么形态被例化的（普通模块、参数生成、接口实例还是库单元）。两侧报告要分开看：reference 侧悬空几乎总是读入集合或配置问题；implementation 侧悬空则首先怀疑库。配套用 report_black_box 列黑盒，黑盒与未解析引用是同一问题的两种记账方式。

2. 读入遗漏与 uselib 库映射。 reference 侧的小写模块名，先在仓库 grep 模块定义：存在就是 filelist 漏读或读入顺序错（SystemVerilog package 必须先于使用方读入）；定义位于某个 IP 库目录、RTL 里用 uselib dir=... 声明的，Formality 读入时该目录不在 search_path 上，uselib 解析不到，表现与漏文件完全相同。稳妥做法是不用 uselib 的隐式查找，把库目录里的文件显式列入 filelist，或在读入前补齐：

tcl
set_app_var search_path [concat $search_path ./ip/fifo/rtl ./rtl]

Linux 文件名大小写敏感，从 Windows 目录同步来的 filelist 要用真实文件名逐个对一遍；同名模块在两个 IP 里各有一份时，后读入的静默覆盖先读入的，grep 到多处定义就要分容器或改名。

3. parameter、define 与条件例化：引用在某个配置下本就不该存在。 这是 LEC 场景特有的一类「假悬空」。RTL 用 generate 按 parameter 决定例化哪个子模块，或用 ifdef CFG_A 包裹例化语句，当 reference 与 implementation 两侧读入时参数/宏不一致，一侧例化了 arbiter_dyn、另一侧该分支根本没生成，link 就报一侧悬空、随后出现 Reference-only 模块。先对两侧配置：

tcl
report_parameter -r
report_parameter -i

宏开关则逐条 diff 两条 read_verilog 命令上的 -define 集合。确属同一设计的不同配置错误时，对齐参数与宏后重读；若是有意为之的配置裁剪（formal 只验某个功能域），用 set_dont_verify 显式排除该锥并在评审记录里写明理由，绝不靠留一个黑盒蒙混过去。

4. 工艺库一致性：网表侧的大写单元名。 SDFFRX4 这类悬空名补 RTL 文件毫无作用，它的定义在工艺库 .db 里。处置是 read_db 读入与本次综合同一工艺角、同一库版本的 .db，并确认在 link_library 中：

tcl
set_app_var link_library [list * typical.db sram_tt.db]
read_db ./libs/typical.db
list_libs

两个高频变种：一是网表用了老库单元名（综合后库升级、网表没重跑），.db 里查无此名，正确动作是用同次综合配套的库而不是改网表；二是有人 grep 出悬空单元名随便找个行为级 .v 顶上，link 能过，但单元功能、时序弧与真库不符，verify 结论直接作废。判断依据永远是「网表与库来自同一次综合」。

5. hdlin_unresolved_modules：被静默放过的黑盒。 默认或被脚本设置为 black_box 时，所有找不到定义的模块静默变成黑盒，读入阶段一条 Error 都没有，问题整体推迟到 match——两侧黑盒不一致就产生成片 UID_数字 未映射点，排查者看到的是「对不上」而不是「没读到」，方向极易带偏。新项目 setup 开头显式收紧：

tcl
set_app_var hdlin_unresolved_modules error

这样缺定义在 link 当场失败，迫使问题在最早的时点暴露。确属真实黑盒的硬 IP（SRAM、PLL），走厂商 formal model 并保证两侧同名同数量，黑盒清单与 report_black_box 输出对拍，清单外的黑盒一律回查。黑盒引发的映射失败如何继续定位见 LEC nonequivalent 调试，retime 与寄存器重映射见 LEC retime 寄存器匹配失败。

五、预防与纪律 ​

  • 进 match 前强制归零：setup 脚本末尾对 r/i 两侧各跑一次 report_unresolved_references 与 report_black_box，计数非零即 error 中止，把 Warning 升级成硬门禁。
  • 未解析即失败：显式 set_app_var hdlin_unresolved_modules error，不接受静默黑盒；真实 IP 黑盒走清单化管理。
  • 单一配置来源：filelist、+define+、parameter 由同一份配置驱动仿真、综合与 Formality，两侧读入命令做 diff 评审。
  • 库与网表同源归档：综合产物、.db、SVF 同目录打包，Formality 启动时校验工艺角与时间戳，禁止拿异库顶 link。
  • 少用隐式查找：uselib、通配 filelist 改为显式文件列表，跨平台同步后核对大小写。

这一篇在知识体系里的位置 ​

本篇是 EDA 排错速查簇中「link 阶段引用解析」节点的 FAQ 页：读文件阶段的失败见 Formality 模块/单元找不到，include/工艺库/IP 模型等外部依赖视角见 Formality 依赖缺失；setup-match-verify 的完整方法见 形式验证（二）：LEC/Formality，引用悬空诱发未映射点后的调试顺序见 LEC nonequivalent 调试，retime 深水区见 LEC retime 寄存器匹配失败，总入口见 EDA 开源与报错索引。

一句话总结 ​

Formality 引用无法解析发生在 link 之后：先用 report_unresolved_references -r/-i 按悬空名定性，全小写 RTL 模块名回 filelist 查漏文件、uselib 目录与 define/parameter 配置，全大写单元名用同次综合配套的 .db read_db 补库而非补 RTL；务必把 hdlin_unresolved_modules 设为 error、进 match 前让未解析引用与两侧黑盒差异归零，否则悬空引用会以 UID 未映射点在 match 阶段爆发，verify 结论不覆盖这些锥。