企业官网建设流程全解析

1. 先搞清楚 Formality 到底在比什么

Formality 这类形式验证工具，本质上是在做一件事：把 RTL 和综合后的网表都转成统一的数学模型，然后逐点证明两边在所有输入组合下行为一致。听起来很美好，但实际跑起来，十个失败里有六七个不是真正的逻辑错误，而是常值（constant）处理不一致导致的假失败。我这些年 debug 下来的体感是，常值问题之所以烦人，是因为它不像功能 bug 那样有明确的波形可追，报错信息往往只给你一个 compare point 失败，剩下的全靠自己顺藤摸瓜。

先说清楚常值问题为什么会成为重灾区。RTL 里你写assign a = 1'b0;，综合工具看到这个信号永远为 0，很可能直接把它优化掉，或者在网表里把它 tie 到某个 constant 网络上。但 Formality 在匹配阶段，如果两边的常值处理策略不一致——比如 RTL 侧认为这是个有名字的 net，网表侧已经把它 merge 进了某个 tie cell——匹配点就对不上，验证直接挂掉。更隐蔽的情况是，某些信号在 RTL 里是常量，但经过综合优化后变成了 floating 或者被传播到了下游逻辑里，Formality 找不到对应的 compare point，报 unmatched。

这类问题的核心矛盾在于：综合工具的优化自由度和形式验证的等价性要求之间存在天然张力。综合工具为了面积和时序，会做 constant propagation、dead logic elimination、tie cell insertion 等一系列操作，而 Formality 期望的是一个相对忠实的结构映射。两者之间的 gap，就是常值问题滋生的土壤。

我见过太多人一看到 Formality 失败就慌了，开始怀疑 RTL 写错了，花大半天追功能波形，最后发现只是某个1'b0被优化掉了。所以这篇东西的目标很明确：把常值导致的 Formality 失败拆成几类典型场景，给出可复现的 debug 路径，让你下次遇到类似报错能十分钟内定位到根因，而不是盲目地翻 RTL。

适合谁看？做过基本综合流程、跑过 Formality 但一遇到失败就卡壳的验证或后端同学。如果你还没接触过 Formality，建议先把基本的 setup 和 match 流程跑通再来看这篇，不然容易一头雾水。

2. 常值问题的四类典型场景拆解

2.1 场景一：RTL 常量被综合直接 tie 掉

这是最常见的一类。RTL 里某个信号被赋了固定值，综合工具在 elaborate 阶段就把它 constant fold 掉了，网表里根本不存在这个信号对应的 net，取而代之的是一个 tie-high 或 tie-low cell 的输出。Formality 在 match 阶段拿 RTL 的 net 名去网表里找，找不到，报 unmatched point。

举个我实际踩过的例子。某模块里有个配置寄存器，复位后默认值写死为8'h00，RTL 里是assign cfg_reg = 8'h00;。综合后这个信号被完全消除，下游用到它的地方直接接了常量 0。Formality 跑出来一堆 unmatched，报错指向cfg_reg相关的 compare point。第一次遇到时我以为是综合脚本哪里配错了，后来才明白这是综合工具的正常优化行为。

处理这类问题的关键不是阻止优化，而是让 Formality 理解这种优化是合法的。具体做法是在 Formality 的 setup 阶段用set_constant命令显式声明这些信号在两边都是常量，或者在综合脚本里加set_dont_touch保留这些 net。两种方案各有取舍：set_constant更轻量，不影响综合结果；set_dont_touch会牺牲一点面积和时序，但结构更忠实。我的习惯是优先用set_constant，只有在后续还需要对这些信号做 ECO 或者 debug 时才考虑set_dont_touch。

注意：set_constant的作用域要写清楚，是只对 RTL 侧生效还是两侧都生效。如果只对一侧设了常量，另一侧还是普通 net，匹配照样会出问题。

2.2 场景二：Tie cell 插入导致的匹配断裂

综合工具在把常量传播到下游时，通常不会直接把常量值写进逻辑门的输入，而是插入专门的 tie-high/tie-low cell。这些 cell 的输出在网表里是一个真实的 net，但 RTL 侧对应的可能是一个直接赋值的 wire。Formality 在做 compare point 匹配时，如果 tie cell 的输出 net 没有被正确识别为常量源，就会把它当成普通信号去匹配，结果自然是找不到对应点。

这类问题的典型特征是：报错集中在某些特定模块的输入端口附近，而且失败的 compare point 往往和时钟、复位或者配置信号相关。我遇到过一次，某个模块的 enable 信号在 RTL 里是assign en = 1'b1;，综合后变成了一个 tie-high cell 驱动。Formality 报en这个 net 在网表侧是 unmatched，但网表里明明有个 tie cell 输出叫en_tie。问题就出在名字变了，匹配算法没认出来。

解决办法有两个层面。第一层是在 Formality 里用set_match_compare或者set_user_match手动建立 RTL net 和网表 tie cell 输出之间的对应关系。第二层更根本，是在综合脚本里控制 tie cell 的命名规则，让综合工具在插入 tie cell 时保留原始信号名作为前缀，这样 Formality 的自动匹配更容易命中。我一般会在综合脚本里加类似set tie_cell_name_prefix的配置（具体命令名各工具不同，这里说的是思路），让 tie cell 的输出名带上原信号名，匹配成功率会高很多。

2.3 场景三：常量传播跨越模块边界

这个场景比前两个隐蔽得多。综合工具做 constant propagation 时，不会局限于单个模块内部，它会沿着层次结构把常量往下游推。比如顶层某个输入端口被 tie 成常量，综合工具会把这个常量一路传播到子模块内部，把子模块里依赖这个输入的逻辑全部优化掉。Formality 如果按层次做匹配，子模块的 compare point 数量会和 RTL 对不上，报大量 unmatched。

我印象最深的一次是某个跨层次的设计，顶层有个 test mode 信号在功能模式下固定为 0，综合后整个 test logic 被优化掉。Formality 跑层次化验证时，子模块里和 test 相关的 compare point 全部失败。当时第一反应是综合把功能逻辑也误删了，后来用report_unmatched_points仔细看，发现失败的全是 test 相关路径，功能路径完好，才确认是常量传播的正常行为。

处理这类问题的思路是：在 Formality 里用set_constant在顶层声明这些跨层次常量，让工具知道这些信号在两边都是常量，从而跳过对相关 compare point 的严格匹配。同时，如果设计里有明确的 test mode 或配置模式，建议在综合和 Formality 的 setup 里都显式声明这些 mode 的常量值，保持两边一致。这里有个经验：常量传播导致的 unmatched，往往集中在特定功能模式下才会激活的逻辑上，如果你发现失败点有明显的功能聚集性，优先怀疑常量传播。

2.4 场景四：Floating net 被误判为常量

这一类比较特殊，严格说不是常量问题，但表现和常量问题很像。综合工具在某些情况下会把没有驱动或者驱动被优化掉的 net 变成 floating，而 Formality 在比较时可能把 floating 当成一个不确定值，导致 compare point 失败。更麻烦的是，有些工具会把 floating net 默认 tie 到某个值（通常是 0），如果 RTL 侧这个 net 有明确驱动，两边就不一致了。

我遇到过一次，某个模块的输出端口在某种配置下确实没有驱动，RTL 里是assign out = cond ? data : 1'bz;，综合后1'bz分支被处理成了 floating。Formality 报这个输出端口 compare 失败，波形上看 RTL 侧是高阻，网表侧是 0。这种问题的根因是三态逻辑在综合后的处理策略和 Formality 的期望不一致。

解决这类问题，首先要在 RTL 层面尽量避免不必要的三态逻辑，能用 mux 就用 mux。如果确实需要三态，在 Formality 里用set_floating_net或者类似的命令显式声明哪些 net 允许 floating，并指定比较时的处理策略。另外，综合脚本里对三态的处理选项也要和 Formality 的配置对齐，别一边允许 floating 一边又要求严格匹配。

3. 一套可复用的 Debug 流程

3.1 第一步：用 report_unmatched_points 做初步分类

Formality 失败后，别急着看 RTL，先跑report_unmatched_points把失败点列出来。这个报告会告诉你哪些 point 是 unmatched、哪些是 compare failed、哪些是 not compared。常值问题导致的失败，绝大多数表现为 unmatched 或者 not compared，而不是 compare failed。compare failed 通常意味着真正的逻辑不等价，那是另一个维度的 debug。

拿到报告后，按模块和信号类型做分类。如果失败点集中在某个模块的输入端口，优先怀疑 tie cell 或者常量传播；如果失败点集中在配置相关信号，优先怀疑 RTL 常量被优化；如果失败点里有明显的 test 或 mode 信号，优先怀疑跨层次常量传播。这个分类动作看起来简单，但能帮你快速缩小排查范围，避免大海捞针。

我一般会把报告导出成文本，用脚本按模块名和信号名做聚合统计。比如统计每个模块的 unmatched 数量，数量特别多的模块往往是常量传播的重灾区；再统计失败信号名里是否包含test、mode、cfg、tie等关键词，命中这些关键词的基本可以直接往常量方向查。

3.2 第二步：对照综合日志确认优化行为

Formality 的报告只能告诉你哪里失败了，不能告诉你为什么失败。要确认是不是常值问题，得去看综合日志。综合工具在做 constant propagation 和 dead logic elimination 时，通常会在日志里打印被优化掉的信号列表，或者至少在 report 里能查到某个信号被 tie 到了什么值。

具体操作上，我会在综合脚本里打开详细的优化报告选项，把 constant propagation 和 tie cell insertion 的记录都留下来。然后拿 Formality 的 unmatched 列表去和综合日志做交叉比对，如果某个 unmatched 信号在综合日志里明确记录了被 tie 成常量或者被优化掉，那基本可以确认是常值问题。

这里有个细节要注意：综合日志里的信号名可能是优化后的名字，和 RTL 名不一定完全一致。如果综合工具做了 rename，需要先搞清楚命名映射关系。我一般会在综合脚本里关掉不必要的 rename 优化，或者至少保留原始名的映射信息，方便后续 debug。

3.3 第三步：用 set_constant 做验证性修复

确认是常值问题后，下一步是用set_constant做验证性修复。所谓验证性，就是先不改综合脚本，只在 Formality 侧加常量声明，看失败是否消失。如果加了set_constant后验证通过，说明问题确实出在常量处理不一致上，而不是真正的逻辑错误。

set_constant的写法要注意作用域和值。基本语法是set_constant <signal_name> <value> -type <port|net|pin>，其中 value 可以是 0、1 或者 X。对于 tie-low 的信号用 0，tie-high 的用 1，不确定的用 X。作用域上，如果常量只在 RTL 侧成立，加-rtl选项；只在网表侧成立，加-netlist；两边都成立就不加。我一般会先两边都加，确认问题定位后再收窄作用域。

提示：set_constant加多了会掩盖真正的逻辑错误。如果加了大量常量声明后验证通过，要回头检查这些常量声明是否都合理，别把真 bug 一起盖住了。

3.4 第四步：决定是修综合脚本还是修 Formality 配置

验证性修复通过后，面临一个选择：是改综合脚本保留这些信号，还是改 Formality 配置接受这些优化。这个选择没有标准答案，取决于项目阶段和后续流程。

如果项目还在早期，综合结果还会反复迭代，我倾向于改 Formality 配置，用set_constant把这些常量声明固化到验证脚本里。这样综合工具可以自由优化，Formality 侧通过常量声明来对齐，两边各司其职。如果项目已经接近 signoff，综合结果基本冻结，可以考虑在综合脚本里对关键信号加set_dont_touch，让结构更忠实，减少后续 ECO 的风险。

还有一个折中方案：在综合脚本里控制 tie cell 的命名和常量传播的粒度，让优化行为更可预测，同时在 Formality 侧保留最小必要的常量声明。这个方案需要两边配合调整，工作量稍大，但长期看最稳。我现在的习惯是，新项目一开始就把 tie cell 命名规则和常量传播策略定好，Formality 脚本里只保留少量必要的set_constant，大部分靠自动匹配解决。

4. 实操中踩过的坑与排查速查表

4.1 那些年踩过的常值坑

第一个坑是set_constant的值写反了。有次某个信号在 RTL 里是 tie-high，我在 Formality 里手滑写成了 0，结果验证倒是通过了，但后来发现网表侧实际是 1，等于用错误的常量声明掩盖了真实的不一致。这个坑的教训是：加完set_constant后一定要回头核对值，别只看验证通过就完事。

第二个坑是常量声明的作用域搞混了。有次我只在 RTL 侧加了set_constant，网表侧没加，结果 Formality 认为两边不一致，报 compare failed。当时以为是逻辑错误，查了半天才发现是作用域问题。后来我养成了习惯，加常量声明时先想清楚这个常量在两边是否都成立，不成立的话分别加。

第三个坑是跨层次常量传播没考虑到。有次顶层某个 mode 信号固定为 0，综合后子模块里相关逻辑被优化，Formality 层次化验证报大量 unmatched。我一开始只在子模块层面加set_constant，没效果，后来才意识到要在顶层加，让常量声明沿着层次往下传。这个坑说明常量声明的位置很重要，跨层次问题要在跨层次的层面解决。

第四个坑是 floating net 和常量的混淆。有次某个 net 在网表里是 floating，Formality 默认把它当 0 处理，和 RTL 侧的高阻不一致。我一开始按常量问题处理，加set_constant没解决，后来才明白要用 floating net 相关的配置。这个坑提醒我，看到 compare failed 先别急着归类，确认清楚是常量、floating 还是真正的逻辑不等价。

4.2 常值问题排查速查表

4.3 几个提升效率的小技巧

第一个技巧是写一个脚本自动解析 Formality 的 unmatched 报告，按模块和信号名关键词做聚合。我用的脚本很简单，就是 grep 加 awk，把报告里的信号名提取出来，按模块分组统计数量，再按关键词（test、mode、cfg、tie、const）打标签。这个脚本帮我省了大量手工翻报告的时间，尤其是失败点上百个的时候。

第二个技巧是在综合脚本里统一 tie cell 的命名前缀。不同综合工具的命令不一样，但思路都是让 tie cell 的输出名带上原始信号名。这样 Formality 的自动匹配算法更容易把 RTL net 和网表 tie cell 输出对应起来，减少手工 user match 的工作量。

第三个技巧是维护一个项目级的常量声明清单。每次遇到常值问题并解决后，把对应的set_constant声明记录到清单里，注明信号名、值、作用域和原因。下次综合结果更新后，直接拿清单去核对，不用重新排查一遍。这个清单在项目后期特别有用，因为那时候综合迭代频繁，常值问题容易反复出现。

第四个技巧是分层验证时先跑 flat 模式确认问题范围。层次化验证虽然快，但常值问题在层次化模式下表现得更复杂，容易误判。我一般会先用 flat 模式跑一遍，确认失败点是否和层次相关，再决定用哪种模式深入 debug。flat 模式慢是慢点，但定位问题更直接。

5. 从根上减少常值问题的设计习惯

5.1 RTL 层面能做的预防

常值问题的根源在 RTL 和综合的交互，所以 RTL 层面能做的预防其实不少。第一条习惯是避免在 RTL 里写无意义的常量赋值。比如assign a = 1'b0;这种，如果这个信号后续根本不用，直接删掉；如果要用，考虑是否真的需要这个中间信号，能不能直接在下游用常量。减少 RTL 里的常量信号数量，就减少了综合优化的空间，也减少了 Formality 匹配的复杂度。

第二条习惯是对确实需要保留的常量信号加综合属性。比如某些配置寄存器或者模式信号，虽然值是固定的，但后续可能需要 ECO 或者 debug 时观察，这类信号可以在 RTL 里加dont_touch或者keep属性，让综合工具保留它们。属性写法各工具有差异，但思路一致：明确告诉综合工具哪些常量不能优化。

第三条习惯是统一常量的表达方式。项目里有的地方写1'b0，有的地方写1'b1，有的地方用 parameter 定义常量，风格不统一会增加综合优化的不确定性。我一般会在项目规范里约定：功能相关的常量用 parameter 统一定义，test 相关的常量单独分组，避免混在一起被综合工具一锅端。

5.2 综合脚本的配置要点

综合脚本里和常值相关的配置主要有三块：constant propagation 的控制、tie cell 的命名、以及优化报告的详细程度。constant propagation 一般不建议完全关掉，那样面积和时序损失太大，但可以控制传播的层次深度，避免跨太多层次导致 Formality 匹配困难。tie cell 命名前面说过了，统一前缀是关键。优化报告一定要打开，尤其是 constant propagation 和 dead logic elimination 的记录，这些是后续 debug 的依据。

还有一个容易被忽略的点是综合和 Formality 的常量值要一致。比如综合时某个 mode 信号按 0 处理，Formality 里也要按 0 声明，别一边 0 一边 1。这个一致性看起来是常识，但实际项目里因为脚本版本不同步导致的不一致我见过好几次。建议把常量值定义放在一个共享的配置文件里，综合和 Formality 都从这个文件读，避免手工同步出错。

5.3 Formality 脚本的维护策略

Formality 脚本里的常量声明建议按模块分组管理，每个模块一个 section，注明每个声明的来源和原因。这样综合结果更新后，可以快速定位哪些声明需要复核。我一般会在脚本里加注释，格式是# <signal_name>: <value> because <reason>，reason 写清楚是 tie cell、常量传播还是 floating 处理。

另外，set_constant声明要定期清理。项目推进过程中，有些常量声明可能因为 RTL 改动或者综合策略调整而失效，留着不仅没用还可能掩盖新问题。我一般每个综合迭代周期清理一次，把不再需要的声明删掉，保持脚本精简。

最后一个策略是保留一个最小可复现的 debug 环境。遇到常值问题时，把相关的 RTL 片段、综合配置和 Formality 脚本抽出来，做成一个独立的小案例。这样下次遇到类似问题可以直接在这个环境里快速验证，不用在完整设计上反复跑。这个习惯帮我省了很多时间，尤其是那种偶发的、和特定综合选项相关的常值问题。

6. 一个完整的排查实例复盘

6.1 问题现象与初步判断

某次综合后跑 Formality，报了一百多个 unmatched point，集中在三个子模块。初步看报告，失败信号名里大量包含cfg和mode关键词，还有一部分是模块输入端口。第一反应是常量传播导致的，但不确定是 tie cell 问题还是跨层次传播问题。

先跑report_unmatched_points做分类，发现三类失败点：第一类是cfg_*信号，在 RTL 里是固定值赋值；第二类是模块输入端口，网表侧对应的是 tie cell 输出；第三类是几个mode_*信号，跨层次出现在多个子模块里。这个分类结果指向两个方向：cfg 信号是 RTL 常量被优化，输入端口是 tie cell 匹配问题，mode 信号是跨层次常量传播。

6.2 逐类定位与修复

先处理 cfg 信号。查综合日志，确认这些信号在 elaborate 阶段被 constant fold 掉了，网表里不存在对应 net。在 Formality 里对这些信号加set_constant，值按 RTL 里的赋值填，作用域两边都加。加完后重跑，cfg 相关的 unmatched 全部消失。

再处理输入端口。查综合日志，确认这些端口在网表侧由 tie cell 驱动，但 tie cell 输出名和 RTL 端口名不一致。这里没有改综合脚本，而是在 Formality 里用set_user_match手动建立 RTL 端口和网表 tie cell 输出的对应关系。手动匹配了十几个点后，这部分失败也解决了。

最后处理 mode 信号。这类信号在顶层固定为 0，综合后传播到子模块。在顶层加set_constant声明，值填 0，作用域两边都加。重跑后子模块里的 mode 相关 unmatched 消失。这里有个细节：顶层声明后，子模块层面不需要重复声明，常量会沿着层次自动生效。

6.3 复盘与经验沉淀

这次排查总共花了不到两个小时，其中大部分时间在查综合日志和核对信号名。复盘下来，有几个经验值得记下来。第一，report_unmatched_points的分类动作非常关键，它把一百多个失败点拆成了三类，每类的处理方式不同，如果混在一起查会很乱。第二，综合日志的详细程度直接影响排查效率，这次能快速定位是因为日志里记录了 constant propagation 和 tie cell 的详细信息。第三，set_user_match虽然能解决问题，但手工匹配十几个点还是有点烦，后续考虑在综合脚本里统一 tie cell 命名规则，减少手工匹配的工作量。

这次排查后，我把相关的set_constant和set_user_match声明整理进了项目级的常量声明清单，并在综合脚本里加了 tie cell 命名前缀的配置。下一个综合迭代周期再跑 Formality，同类问题没有再出现。这个闭环让我更确信：常值问题的 debug 不只是解决当下，更要把经验沉淀成配置和规范，让问题不再反复。

7. 关于常值 debug 的一点个人体会

做 Formality debug 这些年，我最大的体会是：大部分失败不是设计错了，而是两边的“语言”没对上。常值问题尤其如此，综合工具和形式验证工具对同一个信号的理解可能完全不同，一个认为它是可优化的常量，一个认为它是需要严格匹配的 net。debug 的本质就是当翻译，把两边的语义对齐。

另一个体会是，别把set_constant当成万能药。它确实能快速让验证通过，但用多了会掩盖真实问题。我现在的原则是：每加一个常量声明，都要能说清楚为什么加、值为什么是这个、作用域为什么这么设。说不清楚的，宁可多花时间查清楚，也不盲目加声明。

最后分享一个小习惯：每次 Formality 失败，不管最后是不是常值问题，我都会在项目笔记里记一笔，写清楚现象、排查路径和最终根因。积累下来，这些笔记成了我自己的排查知识库，下次遇到类似现象能直接翻笔记，比从头查快得多。常值问题看着琐碎，但把每次踩坑的经验沉淀下来，慢慢就能形成一套自己的 debug 方法论，遇到新问题也不慌。