Formality 未定义符号：Cannot resolve reference 速查
更新时间：2026-10-23。FAQ 速查页，属于 EDA 工具排错系列，总入口见 EDA 开源与报错索引。Formality（
fm_shell，Synopsys 形式验证工具）读入设计后要把例化的每个模块名解析到某个真实定义——RTL 文件、工艺库单元或 IP 库单元。解析不到的就是「未定义符号」，断点集中在链接（link）阶段。本篇按报错原文逐条收敛；模块整体读不进来的相邻问题见 Formality 模块/单元找不到速查，license 层失败见 Formality license 检出失败。
本文要回答的问题
Can't resolve reference和Unresolved references断在 Formality 读流程的哪一步？- 符号明明在某个 .v 里定义了，为什么 link 时还是解析不到？
link_library/search_path配错时分别是什么现象？- SystemVerilog package、宏开关、extern 声明类的符号为什么最容易丢？
- 黑盒（black box）和「真缺定义」怎么区分？
一、报错原文与现象
Formality 的「未定义符号」有四个高频形态，先认清再动手：
Error: Can't resolve reference 'fifo_sync' in design 'top'. (UID-95)
Warning: Unresolved references during link of design 'top': 3.
Error: Can't open file '../libs/typical.db' for reading.
Information: Design 'top' was successfully linked with 2 black boxes.第一句是典型锚点：链接 top 时有个例化名 fifo_sync 找不到定义，UID 类编号是 Formality 标准格式。第二句是汇总告警：一批引用没解析，具体清单要用报告命令展开。第三句断在更外层——连库文件都没打开，不是符号问题而是文件路径问题。第四句最隐蔽：链接「成功」了，但带了 2 个黑盒，未定义符号被静默吞成了黑盒，到 match 阶段才以映射失败爆发。
一句话根因：链接时 Formality 拿着例化名去「已读入的 RTL 定义 + link_library 里的库单元」两个集合里查名，两个集合都查不到就是未定义符号；要么定义没读进来，要么库没挂上，要么名字对不上。
二、原因速查表
| 报错现象 | 可能原因 | 处置 |
|---|---|---|
| Can't resolve reference（RTL 模块名） | filelist 漏文件、该文件未读入 | 补进 read_verilog 列表，按依赖顺序重读 |
| Can't resolve reference（std cell/IP 名） | link_library 未加载对应 .db | read_db 补库，list_libs 确认 |
| Can't open file for reading（.db） | search_path 漏目录、相对路径基准错 | 补 search_path 或用绝对路径 |
| Unresolved references（package 类型） | SystemVerilog package 读入顺序在使用之后 | 先读 package 再读模块 |
| Unresolved references（ifdef 内定义） | 读入未传对应宏开关，定义被预处理剔除 | read_verilog 加与综合一致的宏定义 |
| 链接成功但带 black box | 变量把未解析模块静默转黑盒 | report_black_box 核对，回 filelist 补定义 |
| extern 声明找不到实体 | 只有接口声明，实现文件漏读 | 补实现文件；确属外部 IP 则显式列黑盒 |
| 库单元名解析不到且库已加载 | .db 版本与工具不符、库内无该 cell | 换匹配版本的 .db，查库内容清单 |
三、排查决策路径
按「文件能开 → 定义读入 → 库挂上 → 名字对上」的顺序收敛，任何一步不过就在那一步修：
读这张图抓住一条主线：红色入口往下，四个蓝色判定逐级证明「文件能开、定义读入、库挂上、名字对上」，任何一级不过都落到橙色的补读/补库修复，全过才进绿色的 match；紫色是收尾的防复发动作。颜色只表达角色：红是现象入口，蓝是排查判定，橙是修复，绿是通过，紫是沉淀。顺序不能反——库没挂上就去查名字一致性，只会越查越乱。
四、逐条排查展开
1. 先证明文件能打开。 Can't open file 先于一切处理：相对路径相对于启动 fm_shell 的工作目录，不是脚本所在目录。稳妥做法是脚本开头解析脚本自身路径再拼绝对路径，或把源目录与库目录都加进 search_path：
set_app_var search_path [concat $search_path ./rtl ./libs]
read_db ./libs/typical.db
read_verilog -r {pkg.sv fifo_sync.v top.v}库文件打不开时 read_db 直接报错，后面所有 std cell 引用都会跟着解析不到，所以这条永远第一个修。
2. RTL 侧符号：九成是漏文件或顺序错。 例化名是项目自己的模块（如 fifo_sync）时，先在仓库里 grep 定义是否存在；存在就补进 read 列表。SystemVerilog 有强顺序依赖：package 必须先于使用它的模块读入，typedef/interface 同理。Linux 文件名大小写敏感，从 Windows 共享目录拿来的 filelist 要用 find . -iname 对一遍真实文件名。
3. 宏开关吞掉定义。 定义被条件编译包住而读入时没传对应宏，文件读了、定义却被预处理器剔掉，现象与漏文件一模一样：
read_verilog -r -define {USE_SYNC_FIFO,ASIC} {fifo_sync.v top.v}核对 read 命令的宏集合与仿真、综合是否一致——三方宏集合不齐是跨工具「这边能链那边不能链」的头号原因。
4. extern / 声明与实现分离。 有些流程里子模块只有接口声明先读入、实现后补，或实现根本在另一个交付包里。如果报错的名字是这类外部单元，要么补实现文件，要么显式把它列入黑盒清单——不要让它靠变量静默转黑盒。名字改编（name mangling）类问题在 SystemVerilog 参数化模块上也会出现：工具内部把参数特化拼进符号名，例化名与定义名表面一致、内部符号不同，这时要核对参数传递是否走对了路径。
5. 库单元符号：挂在 link_library。 报错的名字若是工艺单元或硬 IP（SDFFRX4、RM_1Kx32 这类），问题不在 RTL filelist 而在库。link_library 里列的每个 .db 都要真实加载成功：
link_library = {"typical.db" "sram_compiler.db"}
list_libs
report_black_boxlist_libs 确认库在；report_black_box 列出所有被当黑盒的模块，与项目预期的黑盒清单（SRAM、模拟宏）对拍，清单外的黑盒一律回查 filelist。库版本与工具版本不符时，加载可能静默失败或 cell 集合不符，用与综合同一套版本的 .db。
6. 收尾：让未解析引用归零再进 match。 链接完成后立刻报告未解析引用，reference 与 implementation 两侧都要为零（或只剩显式登记的黑盒）。带着未解析引用进 match，比较点会以 UID 临时名出现、映射靠猜，verify 结论就没有证明意义。未定义符号与黑盒不一致叠加 retime 时的收尾判读，与 Formality 模块/单元找不到速查 第五节同法。
五、防复发纪律
- filelist 单一来源：reference 与 implementation 的读入清单从同一份脚本生成，杜绝手敲漏文件。
- 读入即检：每次 read/link 后立刻报告未解析引用，非零即中止，不带着伤进 match。
- 宏集合三方对齐：仿真、综合、形式验证的宏定义清单集中维护，diff 为空才放行。
- 库与综合同源：Formality 用的 .db 必须与综合同版本同路径派生，升级工具链时同步校验。
- 黑盒清单显式化：预期黑盒（SRAM/IP）写进项目清单，
report_black_box输出与清单对拍。 - 报错原文存档：完整 Error/Warning 上下文贴进问题单，改一步重读一次，避免多处同改后无法归因。
这一篇在知识体系里的位置
本篇是 EDA 排错速查簇的一员，专注链接阶段的符号解析。模块整体读不进来的相邻角度见 Formality 模块/单元找不到速查，例化引用解析的更细视角见 Formality unresolved reference 速查，启动期环境问题见 Formality license 检出失败；同族依赖缺失问题在 SpyGlass 侧的对应物见 SpyGlass 依赖缺失速查。
一句话总结
Formality 未定义符号的本质是链接时例化名在「已读入 RTL 定义 + link_library 库单元」两个集合里都查不到：先修文件打开（search_path/绝对路径），再按名字归属分流——RTL 模块回 filelist 查漏文件、读入顺序与宏开关，std cell/IP 查 read_db 与 list_libs，extern 声明补实现或显式列黑盒，report_black_box 与未解析引用报告归零后才进 match，并把「读入即检、宏三方对齐、库与综合同源」固化成防复发纪律。