极客工场

Appearance

共 1,551 字预计阅读约 5 分钟

Formality 模块/单元找不到：Warning: Cannot find 速查 ​

更新时间：2026-10-22。FAQ 速查页，属于 EDA 工具排错系列，总入口见 EDA 开源与报错索引。Formality（fm_shell，Synopsys 形式验证工具）做逻辑等价性检查时，要把参考侧 RTL（reference，golden）和实现侧网表（implementation，revised）分别读进两个容器再对拍。「模块/单元找不到」就发生在读入到 match 之间：文件没读进来、读进了错误的容器、顶层选错，或综合把模块优化没了。Formality 的完整 setup-match-verify 流程见 形式验证（二）：LEC/Formality，本篇只做报错收敛；综合侧同名问题可对照 Design Compiler 模块找不到速查。

本文要回答的问题 ​

  • Warning: Cannot find design 和 Unresolved references 各自断在读流程的哪一步？
  • 文件明明 read_verilog 过了，为什么 reference 容器里还是没有这个模块？
  • -r、-i、-s 三个容器选项挂错时分别是什么现象？
  • 综合后模块「消失」了，Formality 为什么找不到，又该怎么判它是正常优化还是真丢了？
  • match 报告里的 UID-... 和 unmapped compare point 与「找不到」是什么关系？

一、报错原文与现象 ​

Formality 的「找不到」有四个高频形态，先认清再动手：

text
Warning: Cannot find design 'u_dma_core' in the current container.
Warning: Unresolved reference 'fifo_sync' in design 'top' during link.
Error: Can't open file '../../rtl/dma/dma_core.v' for reading.
Information: 12 compare points are unmapped. (first: UID_147)

第一句出在 set_top 或容器切换时：链接过了，但当前容器（container）里按名字查不到这个设计，多半是文件读进了另一个容器，或顶层名写错。第二句出在 link 阶段：模块被例化了，但容器内没有它的定义——reference 侧多半是 filelist 漏文件，implementation 侧多半是模块被综合展平/优化掉。第三句断得最靠前：read_verilog 连源文件都没打开，问题在相对路径或 search_path。第四句已经活到了 match 阶段：两份设计里有比较点映射不上，Formality 给它起了 UID_数字 的临时名，这是「对不上」而不是「读不到」，但根因常与上面同源（黑盒、常量传播、retime）。

一句话根因：「文件真读进了正确的容器、容器内链接出了完整层次、set_top 选的是两边都存在的顶层」三段通道断了一段，再往后才是 match 阶段的映射引导问题。

二、原因速查表 ​

报错现象可能原因处置
Can't open file for reading相对路径基准错、search_path 没给目录用绝对路径或补 search_path 重读
Cannot find design in current container文件读进了另一个容器（-r/-i 挂反）report_design -r/-i 核对，重读进正确容器
Unresolved reference（reference 侧）RTL filelist 漏文件、package/analyze 顺序错补文件，按 package→子模块→顶层顺序重读
Unresolved reference（实现侧）模块被综合展平或优化掉查综合 log 与 SVF，属正常则靠 SVF 引导
set_top 报找不到顶层名拼错、大小写不符、读入静默失败先 report_design -r/-i 看实际有哪些设计
报工艺单元/IP 名找不到link_library 缺 .db 或 .db 路径错read_db 补库，list_libs 确认
找不到但无 Warninghdlin_unresolved_modules=black_box 静默吞查 report_black_box，缺定义回 filelist 补
一堆 UID 未映射黑盒不一致 / 重命名 / retime 导致核对黑盒清单，读入同次综合的 SVF

三、排查决策路径 ​

按「文件 → 容器 → 链接 → 映射」从外到内收敛，任何一步不过就在那一步修，不要跳步：

eda/ts-formality-module-not-found.md D2 示意图

读图抓住一条主线：红色入口往下，三个蓝色判定逐级证明「读到了、读对了、链接全了」，灰色分支处理库缺失，橙色是各段对应的修复动作。判定顺序不能反——容器没读对就去查 SVF，只会越查越乱。

四、逐条排查展开 ​

1. 先证明文件被读进了正确的容器。 Formality 与 DC 最大的不同是每个 read_* 命令都要指定容器：-r 读进参考侧（golden RTL），-i 读进实现侧（综合网表），-s 读进具名容器做分层比对。挂反是头号低级错——RTL 读进了 -i、网表读进了 -r，set_top 不报错，但 match 时方向全反。读完立刻核对：

tcl
read_verilog -r {pkg.sv fifo_sync.v dma_core.v top.v}
read_verilog -i results/top.mapped.v
report_design -r
report_design -i

两边清单里都应看到 top；只在一侧出现就是挂错或漏读。Can't open file 先于一切处理：相对路径相对于启动 fm_shell 的工作目录而非脚本所在目录，稳妥做法是脚本开头 set RTL_HOME [file dirname [info script]] 后拼绝对路径，或 set_app_var search_path [concat $search_path ./rtl ./ip]。

2. reference 侧 unresolved：九成是 filelist 漏文件或顺序错。 RTL 容器里某模块例化了却没定义，先在仓库 grep 定义是否存在，存在就补进 -r 的读入列表；SystemVerilog package 必须先于使用它的模块读入。VHDL 工程还要核对 read_vhdl 的 library 归属，默认进 work，例化时库名对不上同样报 unresolved。Linux 文件名大小写敏感，从 Windows 共享目录拿来的 filelist 要用 find . -iname 对一遍真实名字。另有两个隐蔽变体：一是同名模块撞车，两个 IP 各带一个 fifo.v，后读入的静默覆盖先读入的，不报错但层次结构是错的那份，grep 定义处数大于一处就要分库或改名；二是 `ifdef 挡住的定义，RTL 在宏分支里而读入时没传 -define，文件读了定义却被预处理器剔掉，表现与漏文件完全相同，要核对读入命令的宏开关与仿真、综合是否一致。

3. set_top 选错与「模块被综合优化掉」。 两侧都读入后要显式声明顶层：set_top r:/work/top 与 set_top i:/work/top。报 Cannot find design 先看 report_design 里的真实名字——综合后顶层可能因 set_top 配置不同而改名，也可能整个子模块被展平（uniquify、inline）进父模块。子模块在网表侧消失不一定是错：综合认为它边界无保留价值就会吸收掉，这时正确做法不是补文件，而是读入同一次综合产出的 SVF 引导文件（set_svf），让 Formality 按综合器的自述重建寄存器映射；只有当综合 log 显示该模块因 set_dont_touch 缺失而被意外删除时，才回综合侧修约束。

4. 库 .db 缺失与静默黑盒。 实现侧 unresolved 的名字若是 std cell 或硬 IP（如 SDFFRX4、RM_1Kx32），问题不在 filelist 而在库：

tcl
link_library = {"typical.db" "sram_compiler.db"}
read_db ./libs/typical.db
list_libs
report_black_box

list_libs 确认库真的加载，report_black_box 列出所有被当黑盒的模块。要特别警惕 hdlin_unresolved_modules = black_box 这个变量：它会让找不到的模块静默变成黑盒、不报错，两边黑盒处理不一致时才在 match 阶段以 UID 未映射爆发。新项目应显式确认该变量取值，黑盒清单（SRAM、模拟宏）与真实缺模块要分开对待。

5. UID 与 unmapped 的收尾判读。 match 后 report_unmatched_points 里出现 UID_数字，说明工具只能按锥结构猜、没按名字配上。先回查黑盒两侧是否一致、set_svf 是否与网表同一次综合产出（错配 SVF 是假不等价的头号原因），retime 严重时再加 set_user_match 手工引导。unmapped 不归零，verify 就没有证明意义。

五、预防与纪律 ​

  • 两侧读入脚本对称生成：reference 与 implementation 各一个 filelist，容器选项 -r/-i 写死在脚本里，杜绝手敲挂反。
  • 读入即检：每次 read 后立刻 report_design 与 report_unresolved_references -r/-i，在进入 match 前让未解析引用归零。
  • SVF 与网表同源管理：把 SVF 当网表的孪生文件归档，跑 Formality 时校验时间戳，错配直接中止。
  • 黑盒清单显式化：SRAM/IP 黑盒写进项目清单，report_black_box 输出与清单对拍，清单外的黑盒一律回查 filelist。
  • 报错原文先存档：完整 Warning/Information 上下文贴进问题单，改一步重读一次，避免同时改三处后不知道哪一步生效。

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

本篇是 EDA 排错速查簇的一员。Formality 的 setup-match-verify 完整方法见 形式验证（二）：LEC/Formality，验证域的概念背景见 验证域 LEC；综合侧的同族报错对照 Design Compiler 模块找不到速查，retime 导致寄存器配不上的深水区见 LEC retime 寄存器匹配失败，不等价点的定位顺序见 LEC nonequivalent 调试。

一句话总结 ​

Formality 模块/单元找不到的本质是「文件读进了正确的容器、容器内链接出完整层次、set_top 选对顶层」三段通道断了一段：先分清报错断在读文件、link 还是 set_top，用 report_design -r/-i 核对容器挂载，reference 侧回 filelist 查漏文件与顺序，实现侧区分「综合正常优化（靠同次 SVF 引导）」与「库 .db 缺失/静默黑盒（read_db 与 report_black_box 处置）」，让未解析引用归零后再谈 match 的 UID 未映射。