Formality 重复定义报错：Duplicate definition of module 速查

更新时间：2026-10-23。FAQ 速查页，属于 EDA 工具排错系列。Synopsys Formality（形式验证工具，命令行外壳是 fm_shell）在 read_verilog/read_db 读入阶段或 set_top 链接阶段发现同一个 module/cell 名出现两份完整定义时，会报 Duplicate definition 或 redefining 告警；轻则后用覆盖前用、留下版本隐患，重则 reference 设计与 implementation 设计各自链接到不同版本，LEC 比对结论直接失真。这类问题的病根几乎都不在 RTL 本身，而在读入顺序、filelist 组织与库管理。工具全貌见 Formality 形式验证实操，相邻问题「模块压根找不到」见 Formality 找不到模块，「符号未定义」见 Formality 未定义符号。

本文要回答的问题

• Duplicate definition of module 'xxx' 里两个来源各是怎么进 fm_shell 的？
• 同一个 .v 文件被 read_verilog 读了两次，为什么有时只是 Warning 有时直接炸？
• .db 库里的 cell 和设计里自写的模块同名，Formality 会信哪一份？
• package 被编译两次导致 set_top 失败，和 module 重复是一回事吗？
• 靠 link_library 声明库与把库文件硬读进来，差别在哪里？

一、报错原文与典型现象

Formality 的重复定义信息进 fm_shell 日志与 report_hdlin_errors 输出，关键特征是同一条信息里给出来源线索——先是哪份定义、这次又是谁撞上。典型文案（模块名与路径已占位）：

1. 同一模块被读入两次（最常见，fm_shell 给出 redefining 提示）：

Warning: redefining module 'uart_rx'
  Previous definition : ./rtl/uart/uart_rx.v
  New definition      : ./legacy/uart_v1/uart_rx.v
  The new definition will be used. (HDL-193)

2. 读入阶段直接报 Error 中断：

Error: Duplicate definition of module 'sync_2ff' found while reading
  './libs/stdcells_model.v'. Module already defined in container 'r'.
  (FM-102)

3. 链接阶段库 cell 与设计模块撞名：

Warning: Design 'pll_wrapper' conflicts with a library cell of the same
  name in link_library; the design definition takes precedence. (LINK-5)

4. package 重复编译（SystemVerilog 工程常见）：

Error: Package 'common_pkg' is being recompiled while an older version
  is still referenced by module 'top'. Elaboration failed. (VER-936)

先分清两条线索：报错里的两个来源是排查的出发点——把它们记下来，后面所有动作都围绕「为什么同时进来」展开；Warning 级与 Error 级要分开态度——HDL-193 这类「新定义覆盖旧定义」的 Warning 不会中断流程，但它意味着设计里藏着两个版本在赛跑，LEC 比的可能根本不是你以为的那份 RTL；FM-102/VER-936 这类 Error 则直接中断读入或链接，不解决就走不到 match 与 verify 那一步。

二、原因速查表

报错现象	可能原因	处置
两个来源是同一个文件	read 脚本里同一文件被 read_verilog 读了两次	读入脚本去重，统一入口
两个来源分属 IP 新旧目录	IP 与本地拷贝/老版本目录同时进 filelist	只保留目标版本目录
撞名一方在 .db 库里	link_library 的库 cell 与设计模块同名	库走 link_library 声明，不硬读；或设计模块改名
撞名一方是 .vh 头文件	`include 的头文件又被 read_verilog 直读	头文件只走 `include，不进读入清单
换宏后出现重复	`ifdef 条件编译让模块在两个分支各定义一份	两份定义互斥化，固定宏组合
package 重编译 Error	同一 package 文件被编译两次且版本不一致	package 先编一次，统一搜索路径
大面积模块同时重复	filelist 递归 -f 互相套娃，同一批文件进两轮	画 include 链，拆重复引用
报错路径含中间输出目录	上次综合/展开生成的网表文件被当 RTL 读进	源清单与生成物目录隔离

三、排查决策树

读这张图抓住「先按两个来源分家」：红色入口是报错本身，蓝色判定只问一句——报错里两份位置是不是同一个文件。同一路径，说明读入组织出了问题，同一文件被读了多轮，去查读入脚本与 filelist；不同路径，说明两份内容在抢同一个名字，去查库、头文件、版本三类撞名。两条橙色修复线分别对应组织层与命名层，紫色收尾是统一复验。

四、逐条排查展开

第一步：对报错里的文件名做计数。 最快的定位动作，拿文件名在读入脚本与所有 filelist 里数出现次数：

grep -rn "uart_rx.v" ./scripts/ ./filelists/

命中两行以上，看是不是 fm_shell 的 Tcl 脚本里 read_verilog 显式读了一次，而 filelist（-f 参数或 read_file -format verilog filelist.f）里又列了一次——「脚本读一遍、清单再读一遍」是 Formality 工程最常见的重复来源。命中只有一行，说明文件本身只进了一条路，转第三步查撞名。

第二步：拆 filelist 递归套娃。 filelist 互相 -f 引用超过两层时，肉眼很难看清谁被引了几次。把所有递归引用捞出来：

grep -rn "^-f\|^-F" ./filelists/

从顶层往下展开，凡同一个 .f 出现在两条链上，它名下的文件都会被读两轮。修法是收敛入口：公共子清单只被引用一次；团队约定每个 .f 只在唯一一处被 -f。Tcl 脚本侧同理：read_verilog 循环里对文件名单去重（lsort -unique）再读。

第三步：同名不同文件，按三类撞名分开处置。 报错里两个路径不同、名字相同，逐一对号：

• .db 库与设计撞名：link_library 里的标准单元或宏 cell（如 pll_wrapper 这类常见封装名）与设计模块同名。正确修法不是把库 .db 用 read_db 读成设计，而是让它只待在 link_library 里——库单元只在设计未定义时才被链接引用，天然避开重复判定；设计侧若是自写占位模块，直接改名更干净。LINK-5 的 Warning 虽然让设计定义优先，但同名本身就是隐患，建议在命名规范里给设计模块加项目前缀。
• IP 新旧版本撞名：ip/uart_v1/ 与 ip/uart_v2/ 同时进读入清单，两边都有 uart_rx。处置是版本收敛——filelist 只挂目标版本，老版本整体摘除；切换版本用变量锚定路径，而不是两张清单并列。
• 头文件被直读：defines.vh 一类文件本应由 RTL 里 include 引入，有人又用 read_verilog直读。若头文件里带模块/package 定义（或经它include 了带定义的文件），同名定义就出现两份。纪律是：只含宏/参数的头文件不进读入清单，清单只列实现文件。

第四步：package 重编译，统一编译顺序。 SystemVerilog 工程的 VER-936 本质是 package 被编译两次且引用方还抱着旧版本。修法是定死编译顺序：所有 package 文件在一个 read_verilog -format sverilog 调用里最先读完，模块文件随后；同一 package 文件全工程只出现一次。多个子系统各自带一份 common_pkg.sv 的，合并为单一权威版本，放到公共目录。

第五步：宏导致的条件双份，改互斥。 报错只在特定宏组合下出现时，典型形态是同一模块在 ifdef FAST_SIM 与 else 两个分支各写了一份定义，而某次跑 Formality 两个宏同时被打开。处置是把两份定义改成互斥（ifndef 守卫或收敛为一份参数化定义），并在 fm_shell 脚本里用 -define` 固定宏组合，不允许互斥宏同时打开。

第六步：干净环境复验。 修完先清容器再重读，避免旧定义残留在内存里干扰判断：

remove_container -all
read_verilog -format sverilog -f filelists/ref.f
set_top r:/WORK/top
report_hdlin_errors

确认日志里 redefining/Duplicate 类信息清零、report_hdlin_errors 无 Error，再进 match/verify。Warning 留着不处理，等于给下一次「比错版本」留门。

五、预防与纪律

• 读入单一入口：reference 与 implementation 两侧各只保留一条读入路径（要么 Tcl 显式读、要么 filelist），禁止混用双通道。
• 库只走 link_library：标准单元与宏 cell 一律 set_app_var link_library 声明，禁止 read_db 把库读成设计容器。
• 头文件不进清单：.vh/.svh 只经 include 引入；读入清单只列 .v/.sv` 实现文件，分工写进工程 README。
• IP 版本单点锚定：filelist 里 IP 路径统一走版本变量，切换改变量，不允许两个版本目录同时出现。
• CI 加重名预检：提交前跑 grep -h "^module" $(cat filelists/ref.f) | sort | uniq -d，有输出即拦截——把重复挡在 fm_shell 启动之前。

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

本篇是 EDA 排错速查簇的一员，同工具相邻问题见 Formality 找不到模块、Formality 未定义符号 与 Formality 引用未解析，工具机制背景见 Formality 形式验证实操，跨工具语义对照见 lint 侧的 SpyGlass 重复定义速查。

一句话总结

Formality 报重复定义先读报错里的两个来源：同一文件是读入组织问题——Tcl 脚本与 filelist 双通道各读一遍、递归 -f 套娃，用 grep 计数并收敛单一入口；不同文件是命名撞车——.db 库 cell 交给 link_library 不硬读、IP 新旧版本只留一版、头文件不进读入清单、package 统一先编一次；修完 remove_container -all 清场重读并跑 report_hdlin_errors 确认清零，长期靠单一读入入口、库声明纪律与 CI 重名预检把重复挡在启动之前。