极客工场

Appearance

共 2,477 字预计阅读约 8 分钟

Formality 依赖缺失：include/工艺库/IP 模型找不到速查 ​

更新时间：2026-10-22。FAQ 速查页，属于 EDA 工具排错系列，总入口见 EDA 开源与报错索引。Formality（fm_shell，Synopsys 形式验证工具）做逻辑等价性检查（LEC，Logic Equivalence Checking）时，要把参考侧 RTL 与实现侧网表分别读进 r/i 两个容器再对拍。「依赖缺失」指的不是某个模块文件没读（那是 Formality 模块/单元找不到的话题），而是读进来的东西本身还引用着外部依赖：include 头文件、SystemVerilog/VHDL package、工艺库 .db/.v、IP 黑盒模型，乃至 DC 写出的 SVF 引导文件。setup-match-verify 的完整流程见 形式验证（二）：LEC/Formality，本篇只收敛「依赖」这一类失败。

本文要回答的问题 ​

  • +incdir+ 头文件、package、工艺库、IP 模型四类依赖缺失，分别断在哪一步、长什么报错？
  • 网表 link 时 Unable to resolve 'SDFFRX4' 这类标准单元名，为什么 filelist 补文件没用？
  • reference 侧和 implementation 侧读入集合不对称，为什么会拖到 match 阶段才爆发？
  • SVF 引导文件算不算依赖？缺了它是报错还是静默配错？
  • search_path、link_library、FORMALITY_HOME 在 Formality 里各管什么？

一、报错原文与现象 ​

依赖缺失按报错断点分两批。第一批断在读入（read/analyze）阶段，源码级依赖没凑齐：

text
Error: Cannot open include file 'regs_defines.vh'.
Error: VHDL unit 'ip_types_pkg' not found in library 'work' during analyze.
Error: Cannot open file './results/demo_top.svf' for reading.

第二批读入不报错、断在 link 与 match 阶段，表现是未解析引用、黑盒和比较点对不上：

text
Warning: Unable to resolve reference 'SDFFRX4' in design 'demo_top' during link.
Warning: 2 black boxes exist in the implementation container: 'rm_sram_1k', 'pll_clk'.
Information: 18 compare points are unmapped (first: UID_203).
Warning: Reference-only modules: 3; Implementation-only modules: 0.

第一批直白：include 文件没在 +incdir+ 搜索路径上；VHDL package 没按「先 package 后例化方」的顺序 analyze；SVF 路径错或忘了归档。第二批更迷惑——网表本身读进来了，但里面的标准单元、硬 IP 名字没有任何定义可解析，Formality 先把它们挂成未解析引用或黑盒，真正爆发是在 match：两侧黑盒集合不一致，工具只能按锥结构猜、给比较点起 UID_数字 的临时名，verify 即使跑起来也没有证明意义。

二、原因速查表 ​

报错线索缺的依赖处置
Cannot open include filefilelist 缺 +incdir+ 目录或目录基准错补 include 目录，用绝对路径重读
package/not found in librarySV/VHDL package 未先读、库归属错package 先 analyze 进 work 或具名库，再读例化方
Unable to resolve 标准单元名工艺库 .db 未读或不在 link_libraryread_db 补库，list_libs 确认
网表中的 .v 行为模型找不到search_path/-v 库目录未给补 search_path 或显式读入厂商 .v
black boxes 含 SRAM/PLLIP 厂商形式模型缺失向 IP 提供方要 formal model，两侧对齐读入
Reference-only/Implementation-only两侧读入集合不对称对称补读，差异项逐项解释
Cannot open .svfDC 引导文件未归档或路径错从同次综合结果取回，set_svf 重读
换机器/新人跑才缺FORMALITY_HOME/模块环境未加载module load 对齐，setup 脚本做存在性断言

三、排查决策路径 ​

先给缺的东西分类，再决定从哪里补；判据顺序不要反，上来就怀疑库坏了是最常见的时间浪费：

eda/ts-formality-missing-dependency.md D2 示意图

读图抓一条主线：红色入口之后，蓝色分诊把缺失物归到三个抽屉——源码级依赖、工艺与 IP、两侧对称与 SVF，三者各自补齐后汇成橙色「重读归零」，最后收进紫色的 setup 脚本化。颜色只表达角色：红=现象，蓝=排查，橙=修复，紫=防复发。

四、逐条排查展开 ​

1. include 与 package：读入顺序就是依赖声明。 Verilog/SystemVerilog 的 include 搜索路径来自 filelist 中的 +incdir+ 条目，多个目录用 + 连接；相对目录同样相对于启动 fm_shell 的工作目录，稳妥做法是脚本开头用 [file dirname [info script]] 拼绝对路径：

tcl
set INC [list $RTL_HOME/include $IP_HOME/rtl/include]
read_verilog -r [concat [glob $RTL_HOME/rtl/*.v] \
    [lmap d $INC { string cat "+incdir+" $d }]]

VHDL 工程里 package 必须先用 read_vhdl（或 analyze）读进对应 library，再读例化它的设计单元；默认进 work，filelist 里写了 library ip_pkg is ... 而读入时没声明 -library ip_pkg，例化方就会报库中找不到单元。判断是否属于这一类很简单：报错符号全小写、是参数/宏/类型名而不是单元例化名，基本就是源码级依赖。

2. 工艺库缺失：filelist 补文件补不好的那一类。 Unable to resolve 'SDFFRX4' 这类名字是标准单元，定义在工艺库 .db（或厂商给的 .v 行为模型）里，不在你的 RTL 仓库。补法是读库而不是补文件：

tcl
set_app_var search_path [concat $search_path ./libs/typical ./ip/sram]
set_app_var link_library [list * typical.db sram_tt.db]
read_db ./libs/typical.db
list_libs

list_libs 确认库真的加载；target_library 是综合侧变量，Formality setup 脚本 source 综合环境时常常一并出现，但网表链接真正看的是 search_path 与 link_library，两者别混。还有一种偷懒做法会埋雷：直接把网表中例化的单元名 grep 出来再随便找个 .v 顶上——工艺角、阈值版本对不上，link 能过，verify 的结论却不可信，缺库永远只补「与本次综合同一工艺角」的那份。.db 与 Formality 版本不配套时报的是格式错误而非找不到，需用配套 lc_shell 重编，不要误判成路径问题。

3. IP 黑盒模型：两侧要黑得一致。 SRAM、PLL 这类硬 IP 没有 RTL 源码，厂商通常单独提供形式验证模型（formal model）。reference 侧例化了 IP 却不读模型，它是黑盒；implementation 侧网表里 IP 是硬宏或一组库单元，形态完全不同——match 时这些锥必然 UID 未映射。正确做法是向 IP 提供方索取 Formality 支持的模型，按厂商说明读入对应容器，然后用 report_black_box -r/-i 对拍：两侧黑盒清单必须同名、同数量，清单外的黑盒一律回查是缺模型还是 filelist 漏读。警惕 hdlin_unresolved_modules = black_box：它会让未解析模块静默变黑盒、读入阶段不报错，把问题推迟到 match。

4. 两侧读入集合对称：LEC 的隐含依赖。 等价性检查的前提是两份设计描述的是同一个东西。辅助模块、test 替身、formal model 只读进一侧，就会出现 Reference-only modules 告警。维护两份结构对称的读入脚本（-r/-i 各一份、容器选项写死），读完用 report_design -r/-i 对模块清单做差集，任何差异都要能说出理由（综合展平属于正常差异，靠下一条的 SVF 解释）。

5. SVF 是依赖，不是可选附件。 DC 综合时写出的 SVF（Setup Verification File）记录了展平、重命名、retime 的对应关系，Formality 用 set_svf 读入。文件缺失会直接报打不开；更危险的是读到错配的旧 SVF——不报错，但寄存器按错误的自述映射，制造假不等价。把 SVF 当网表的孪生文件同目录归档、校验时间戳；retime 严重导致的映射失败背景见 LEC retime 寄存器匹配失败，定位到不等价点后的调试顺序见 LEC nonequivalent 调试。

6. 环境依赖最后查，但要一句话排除。 fm_shell 启动报命令找不到或自带库缺失，多是模块环境没加载：FORMALITY_HOME 指向安装根，DesignWare 等自带库经 hdlin_dwroot 解析。换机失败时 module list 与环境变量在两台机器间 diff，一分钟就能排除，别让它混进依赖排查里干扰判断。

五、预防与纪律 ​

  • filelist 单一来源：include 目录、读入顺序、宏定义由同一份 filelist 驱动仿真、综合与 Formality，杜绝三处各写一套。
  • 读入即检：每次 read 后跑 report_design -r/-i 与 report_black_box -r/-i，进 match 前让未解析引用与黑盒差异归零。
  • 库与模型清单化：工艺角 .db、IP formal model 的版本与来源登记在项目 setup 里，路径用环境变量间接一层，换机只改环境。
  • SVF 孪生归档：网表与 SVF 同次综合、同目录归档，脚本启动时断言文件存在且时间戳晚于综合。
  • setup 脚本自带断言：file exists 检查关键依赖，缺失时明确报「缺哪个库、找谁要」，把新人第一小时的困惑拦在脚本里。

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

本篇是 EDA 排错速查簇的一员。Formality 的 setup-match-verify 完整方法见 形式验证（二）：LEC/Formality，验证域概念背景见 验证域 LEC；模块文件没读进来的同族问题对照 Formality 模块/单元找不到，综合侧的依赖问题对照 Design Compiler 依赖缺失，匹配失败后的深水区见 LEC retime 寄存器匹配失败 与 LEC nonequivalent 调试。

一句话总结 ​

Formality 依赖缺失先按断点分类：读入期的 include/package 靠 +incdir+ 与 analyze 顺序解决，link 期的标准单元名靠 read_db 加 link_library 解决，IP 靠厂商 formal model 且两侧黑盒清单对齐，SVF 当网表的孪生依赖同源归档；再用两侧读入集合对拍和 report_black_box 把未解析与黑盒差异拦在 match 之前，长期靠单一 filelist、库模型清单化与 setup 断言守住全组环境一致性。