极客工场

Appearance

共 2,599 字预计阅读约 9 分钟

Formality 退出码非零：fm_shell exit code nonzero 速查 ​

更新时间：2026-10-23。FAQ 速查页，属于 EDA 工具排错系列。fm_shell -f run.tcl | tee fm.log 跑完，CI 红灯，摘要里只有一句「fm_shell returned exit code 1」——Formality 批处理最迷惑的地方在于：verification 没通过（有 Failing points）也会让退出码非零，而工具本身其实跑得好好的。难的是分清这次非零到底是「工具/脚本死了」还是「两个设计就是不等价」。同类退出码问题在其他工具的对照见 SpyGlass 退出码非零，跑到一半被系统杀掉的场景见 Formality 段错误崩溃。

本文要回答的问题 ​

  • 退出码非零，到底是 verify 失败、Tcl 脚本中断，还是包装层 set -e 误伤？
  • Failing points 和退出码是什么关系？verification succeeded 时退出码一定是 0 吗？
  • CI 里 $? 抓到的是 fm_shell 的还是管道里别的命令的？
  • 怎么用 grep 从几万行日志里捞出真正的第一条 Error？

一、报错原文与现象 ​

bash
# CI 通知
stage lec: fm_shell exited with code 1 (FAILED)
# 日志尾部（看起来 verify 正常跑完了）
  Verification FAILED
  -------------------
  Failing compare points: 2
  Passing compare points: 18417
# 或者另一种：脚本中途断掉
Error: Cannot open file 'ref_design.v' (FILE-002)
run.tcl line 12: command failed

两个特征值得记住：一是日志尾部出现 Verification FAILED + Failing compare points 计数，说明工具没死，是设计不等价，退出码非零是 Formality 的「结果语义」而非故障；二是 Error: 行出现在中段、后面跟着脚本行号，说明是 Tcl 脚本里的某条命令挂了，verify 根本没跑到。还有一种最冤的：fm_shell 本身 exit 0，但包装脚本里 set -e 撞上一条无害的非零返回（比如 grep 没匹配到行），整条流水线跟着红灯——排查时先确认非零究竟是谁返回的。

二、可能原因总览 ​

现象/退出码可能原因处置
非零，尾部有 Failing compare pointsverification 真实失败，设计不等价report_failing_points 逐点分析，修网表或约束
非零，中段有 Error + 脚本行号run.tcl 某命令失败（读文件/匹配/设约束）按行号修脚本或输入文件后重跑
非零，日志尾部 Verification SUCCEEDED收尾命令（写报告/归档/通知）失败被 CI 捕获检查退出码捕获的是哪条命令
非零但 fm_shell 日志全绿包装脚本 set -e 撞上无害非零（grep 空匹配等）给无害命令加 `
124包装层 timeout 到点，不是 Formality 的码按 Formality 超时卡死 处理
139 / Segmentation fault工具崩溃被信号杀按 Formality 段错误崩溃 处理
非零，写到一半磁盘满report 写出失败级联非零按 Formality 磁盘写满 清理后重跑

三、退出码语义先讲清 ​

Formality 的退出码不是单一的「成功/失败」开关，而是三个语义层叠出来的，搞混了就会误判方向：

  • 工具层：fm_shell 进程本身有没有跑完。崩溃（139）、被 timeout 杀（124）、license 签出失败中途退出，都属于这一层——特征是日志没有完整的 verify 结论行。
  • 脚本层：run.tcl 是不是从头执行到尾。任何一条 Tcl 命令失败（读文件、设约束、match）都会让 Formality 以 Error + 行号的形式中止，退出码非零，verify 结论行同样缺失，但日志里有明确的第一条 Error。
  • 结果层：verify 跑完了，结论是什么。Verification SUCCEEDED 表示两个设计在 Formality 的判定下等价，此时退出码为 0；Verification FAILED 表示存在 Failing compare points，默认策略下退出码非零——这不是故障，是 Formality 把「不等价」编码进了退出码；Verification INCONCLUSIVE 表示没跑完（中断/资源不足），介于两者之间，通常也按非零处理。

交互模式下可以用 status 命令随时看当前会话进展到哪一步（设计是否读入、是否 match、是否 verify），批处理出问题时不确定卡在哪一层，就把 run.tcl 前几步在交互模式里重放，用 status 逐步确认。三层分清了，后面的分流就是机械动作：先确认进程善终（工具层），再确认脚本走到底（脚本层），最后才轮到看 verify 结论（结果层）。

四、排查决策图 ​

先把这张图的走法说清楚：第一层按退出码数值分流（124/139 直接出 Formality 范围，1/2 才进日志排查）；第二层在日志里分清「工具死了」还是「设计没过关」——尾部有 Verification FAILED 计数表的是后者，方向是分析 Failing points 而不是修工具。红色是问题入口，蓝色是排查动作，橙色是修复路径，紫色是防复发。

eda/ts-formality-exit-code-nonzero.md D2 示意图

主线只有一句话：先看码值再看日志，日志里先分「工具死」与「设计败」。Verification FAILED 走橙色修复路径分析不等价点；SUCCEEDED 还红灯就去查 CI 捕获错位——两条路互不相通，别拿重跑工具的办法对付真实的不等价。

五、逐条排查展开 ​

第一步：拿到真实退出码，再看日志第一条 Error。 CI 里常见写法 fm_shell -f run.tcl | tee fm.log 有个经典坑：管道后 $? 拿到的是 tee 的退出码，不是 fm_shell 的。要么用 set -o pipefail（bash），要么改成 fm_shell -f run.tcl 2>&1 | tee fm.log; rc=${PIPESTATUS[0]}。拿到真实码之后固定套路：

bash
grep -n "^Error\|Error:" fm.log | head -10
grep -n "Verification SUCCEEDED\|Verification FAILED\|Verification INCONCLUSIVE" fm.log
grep -n "Failing compare points" fm.log

第一条 grep 取最早的 Error——后面一串级联报错的根因都是它。第二条定位 verify 结论行，直接决定走哪条路。

verification FAILED：这是「设计没过关」，不是故障。 Formality 的退出码语义和综合工具不同：verify 跑完、存在 Failing compare points，按默认策略就非零退出。处置方向是分析不等价点：report_failing_points 拉出清单，看是寄存器映射错（名字匹配规则没覆盖 retiming/合并）、常量传播差异，还是约束（set_constant、set_dont_verify）没设对。INCONCLUSIVE（中断/未完成）介于两者之间，多半是资源不够或超时截断，先按超时路径排。把「verify 失败」当工具 bug 反复重跑是最常见的浪费——重跑一万次两个设计也不会变等价。

脚本中段 Error：按行号修，别绕。 run.tcl 里读设计、设参考/实现库、match、verify 任何一步失败，Formality 会以 Error + 脚本行号的形式报出，然后退出非零。常见前三名：文件路径错（相对路径在 CI 工作目录下解析不到）、库变量没设（search_path / link_library 缺项）、命令拼写或参数版本差异。按行号定位到那条命令，单独在 fm_shell 交互模式下重放一遍，交互模式给的错误信息比批处理日志全。

多个 Formality 任务并行回归时，聚合退出码要拆开验。 项目回归常一次跑 reference 对 netlist、netlist 对 scan-stitched 等多组比对，包装脚本聚合成一个退出码上报——只要有一组非零整体就红。这时别在聚合日志里乱翻，逐组单跑二分定位到那一组，再对它用上面的 grep 套路；单跑通过、并行失败的，再查临时目录隔离与计算节点资源竞争。

set -e 误伤与捕获错位：脚本层的两类假红灯。 一类是包装脚本 set -e 后，某条语义无害的命令返回非零（grep 空匹配、ls 了不存在的可选文件）直接把整脚本打死；给这类命令加 || true 显式兜底，或干脆去掉全局 set -e、改在关键命令后显式判定。另一类是 CI 捕获的退出码来自收尾命令（压缩日志、上传报告）而不是 fm_shell——把 Formality 调用与收尾命令的返回值分开捕获、分开上报。

六、预防与纪律 ​

  • pipefail + 显式捕获：set -o pipefail 打底，fm_shell 的返回码用 PIPESTATUS 或分步写法单独取，不靠 $? 猜。
  • 脚本逐命令错误传播：run.tcl 里关键步骤（读库、读设计、verify）后检查 Formality 的状态返回值，失败即带阶段名退出。
  • 失败通知附三行摘要：流水线自动摘出 verify 结论行、Failing 计数、第一条 Error，红灯通知里直接可见，省一轮翻日志。
  • SUCCEEDED 才准进下一步：把「verify 结论行 = SUCCEEDED」作为放行条件，而不是只看退出码为 0——双判据才能同时挡住「工具死了」与「设计败了」。
  • 版本对齐：fm_shell 版本与项目 run.tcl 语法对齐（如 2025.06 系列），版本漂移引入的命令差异见版本不匹配类速查。

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

本篇是 Formality 排错速查簇中「批处理与 CI 集成」节点的 FAQ 页，与 Formality 超时卡死（124 退出码的深层排查）、Formality 段错误崩溃（139/崩溃路径）、Formality 磁盘写满（写报告失败的级联非零）互相衔接；其他工具同类问题对照 SpyGlass 退出码非零。

一句话总结 ​

Formality 命令返回非零先做两层二分：码值上 124/139 出 Formality 范围、1/2 进日志；日志里 Verification FAILED 带 Failing points 是设计不等价、走 report_failing_points 逐点修，中段 Error 带行号是脚本问题、交互模式重放定位，SUCCEEDED 还红灯就查 CI 捕获错位与 set -e 误伤；治本靠 pipefail 加显式捕获、关键命令错误传播、失败通知附三行摘要，让每次红灯一眼分清「工具死了」还是「设计没过关」。