Formality 段错误/崩溃：fm_shell segfault crash 速查
更新时间：2026-10-23。FAQ 速查页，属于 EDA 工具排错系列。Formality（fm_shell）在 read_db、set_top、match、verify 任何一步都可能直接
Segmentation fault (core dumped)退出，log 停在崩溃前的最后一行命令输出，既不报 rule 也不报 design object，是 LEC 跑批里最没有上下文的一类故障。好消息是收敛套路固定：先用退出码和 core 分清「被 OOM killer 杀掉」还是「真踩了非法地址」，再按内存、递归宏与超大结构、版本错配、已知 bug 几条线逐条排。通用的段错误分析见 core dump 分析，Formality 正常用法见 形式验证与 LEC 流程，同类工具的崩溃排查见 SpyGlass 段错误/崩溃速查。
本文要回答的问题
- fm_shell 直接 segfault 没有任何 FM 报错，第一步做什么？
- 怎么区分「内存吃爆被 OOM killer 干掉」和「真的访问了非法地址」？
- match 阶段崩和 verify 阶段崩，怀疑方向有什么不同？
- 怀疑命中已知版本 bug，怎么快速定性并收集上报证据？
一、报错原文与现象
Segmentation fault (core dumped)
fm_shell terminated abnormally, exit code 139
last log line: Formality> match
*** FM-ERROR: internal error, session aborted (rarely seen, often truncated)先认指纹：退出码 139 = 128 + 11（SIGSEGV），是真段错误；137（128+9，SIGKILL）几乎总是 OOM killer 干的，那不是 segfault，要走内存通道；134（SIGABRT）多半是堆破坏或 glibc 检查主动中止。还有一类迷惑现象是「log 看着像崩溃其实是被杀」：set_top 或 match 阶段 RSS 一路涨到机器 RAM 上限，进程悄无声息消失，log 尾部没有任何 FM 报错——这种情况去 dmesg 里一定能找到 OOM 记录。另一条重要线索是崩溃时挂在哪条命令上：fm_shell -f run.tcl 跑批时，log 里最后一条 Formality> 提示符后的命令就是崩溃点，read_db 期崩和 verify 期崩的嫌疑名单完全不同。
二、可能原因总览
| 报错现象 | 可能原因 | 处置 |
|---|---|---|
| 退出码 137，dmesg 有 OOM 记录 | 超大设计 set_top/match 峰值内存超 RAM | 加内存、开 hyper-scale、拆验证层次 |
| 退出码 139 且留下 core | 真段错误（空指针/栈溢出） | gdb 取栈回溯，最小化用例 |
| set_top 后 RSS 直线涨到上限 | 超平铺设计或展开层次打爆内存 | hyper-scale 层次化验证、黑盒 IP |
| 读入特定网表/库就崩 | 递归宏展开或循环 include 打爆解析栈 | 展开依赖查环，改写法 |
| 换 fm_shell 版本后不崩/反而崩 | 命中已知 bug 或版本回归 | 版本二分，报厂商要 patch |
| svf 一加载就崩 | svf 引导文件损坏或与版本不配套 | 用配套 svf 重跑，重新生成 |
| 崩溃前磁盘报警 | 磁盘满导致中间文件写半截 | 清空间，删残留重跑 |
| 升级版本后旧 session 恢复崩 | 保存的 session/容器与新二进制不兼容 | 清 session，从头重建流程 |
三、排查决策图
崩溃发生后别急着重跑碰运气，先按下图把「谁杀的、崩在哪一步、向哪条线收敛」定下来。图中颜色按语义分角色：红色是崩溃入口与根因，蓝色是排查动作，橙色是修复，紫色是收尾沉淀。
fm_shell崩溃退出 -> 分谁杀的: 退出码与dmesg与core
分谁杀的: 退出码与dmesg与core -> 137被kill: 查OOM与set_top峰值RSS
分谁杀的: 退出码与dmesg与core -> 139真段错误: gdb取bt定位崩溃阶段
137被kill: 查OOM与set_top峰值RSS -> 修复: hyper-scale或加内存降峰值
139真段错误: gdb取bt定位崩溃阶段 -> read期崩: 查递归宏与循环include
139真段错误: gdb取bt定位崩溃阶段 -> match或verify期崩: 最小化用例加版本二分
read期崩: 查递归宏与循环include -> 修复: 解开宏环与循环依赖
match或verify期崩: 最小化用例加版本二分 -> 修复: 换版本或打patch
修复: hyper-scale或加内存降峰值 -> 归档: 证据包沉淀与流程纪律
修复: 解开宏环与循环依赖 -> 归档: 证据包沉淀与流程纪律
修复: 换版本或打patch -> 归档: 证据包沉淀与流程纪律
fm_shell崩溃退出.style: { fill: "#FDECEC"; stroke: "#D9534F" }
分谁杀的: 退出码与dmesg与core.style: { fill: "#EAF2FE"; stroke: "#3B6FD4" }
137被kill: 查OOM与set_top峰值RSS.style: { fill: "#EAF2FE"; stroke: "#3B6FD4" }
139真段错误: gdb取bt定位崩溃阶段.style: { fill: "#EAF2FE"; stroke: "#3B6FD4" }
read期崩: 查递归宏与循环include.style: { fill: "#EAF2FE"; stroke: "#3B6FD4" }
match或verify期崩: 最小化用例加版本二分.style: { fill: "#EAF2FE"; stroke: "#3B6FD4" }
修复: hyper-scale或加内存降峰值.style: { fill: "#FEF3E2"; stroke: "#E08A1E" }
修复: 解开宏环与循环依赖.style: { fill: "#FEF3E2"; stroke: "#E08A1E" }
修复: 换版本或打patch.style: { fill: "#FEF3E2"; stroke: "#E08A1E" }
归档: 证据包沉淀与流程纪律.style: { fill: "#F1ECFD"; stroke: "#7A5BD4" }读这张图抓住主线：第一步永远用退出码 + dmesg + core 三件事把 OOM 误杀（137）和真段错误（139）分开——137 直接走内存通道，量峰值、开 hyper-scale；139 才用 gdb 对 core 取栈回溯，按崩溃阶段分流：read/elaborate 期崩查递归宏与循环 include，match/verify 期崩走「最小化用例 + 版本二分」判已知 bug。三条修复线最后都要落到证据包沉淀，而不是一句「fm_shell 又崩了」。
四、逐条排查展开
先分清谁杀的，这是总分流阀。 崩溃后立刻做三件事：看退出码（139 / 137 / 134）；dmesg | tail -50 找 OOM killer 记录；确认 core 是否生成（ulimit -c 是否为 0、core 落盘目录是否可写且有配额）。有 OOM 记录就走内存通道，139 且有 core 才是真段错误，往下用 gdb fm_shell core 取 bt 栈回溯，看栈顶落在读入解析、match 还是 verify 的内部符号上，崩溃阶段一目了然。
超大设计的内存画像要先量出来。 Formality 做全芯片平铺 LEC 时，set_top 把参考设计与实现设计同时 elaborate，峰值内存冲到几十 GB 很常见，机器 RAM 或队列配额不够就会被杀。别凭感觉说「设计太大」，用 /usr/bin/time -v fm_shell -f run.tcl 或跑批时挂 pidstat 记录峰值 RSS，和设计规模建对照。峰值贴着 RAM 上限抖动的，先降内存压力：改用 hyper-scale 层次化流程把设计按层次切块验证、黑盒掉不关心的模拟 IP、关掉不需要的 verification 选项。内存问题不解决，后面所有「段错误」都可能是 OOM 的变种。
递归宏与循环 include 会打爆解析栈。 read_verilog / read_vhdl 阶段对宏互相递归展开、include 套 include 没有深度保护，栈打爆就表现为段错误。特征是小设计不崩、读到某个文件必崩、且崩溃点在 read 早期。排查：展开 include 依赖树看有没有环（A include B、B 又 include A），宏定义互相嵌套的改成手动展开。语法类问题的前置排查见 SpyGlass 语法解析失败速查（解析栈问题是各家 EDA 通病）。
版本二分是最便宜的「是不是已知 bug」判据。 手头有相邻两三个版本的 fm_shell（如 2025.06 与前一个小版本）：同一最小用例旧版不崩新版崩，是新版本回归，短期回退顶住并报 bug；新版不崩旧版崩，说明 bug 已修，升级或打 patch 即可。三次运行定性，比任何调试都快。版本错配另有一条：升级后别复用旧版保存的 session/容器文件，格式不兼容会在 restore 时段错误，处置是清掉 session 从头建流程。版本类问题另见 Formality 版本不匹配速查。
svf 引导文件是 Formality 特有的崩点。 svf（setup verification for Formality）记录综合阶段对设计的变换，fm_shell 靠它引导 match。svf 文件损坏、与当前 fm_shell 版本不配套、或综合与 LEC 跨版本生成的，都可能在加载早期触发内部断言或段错误。特征是去掉 svf 就不崩、加上就崩。处置：用与综合、fm_shell 同代配套的 svf 重跑，必要时让综合侧重新生成。
最小化用例是上报证据的核心。 在 set_top 之后逐层裁剪：二分砍设计（只留崩溃相关的层次分支）、砍 svf、砍约束，直到几十到几百行网表能稳定复现崩溃。配合 core 的 bt 输出、log 尾部、版本与环境快照，就是向厂商报 bug 的完整证据包。磁盘满引发的「写半截文件延迟爆炸」也别漏：崩溃后先 df -h 看工作目录与 /tmp，满了清空间删残留重跑，资源类问题另见 SpyGlass 资源超限速查。
五、预防与纪律
- 跑批默认开 core 保留：作业模板里
ulimit -c unlimited，core 目录落在可写、有配额的盘上，崩溃即有现场。 - 内存峰值建档：每个设计 set_top/match 的峰值 RSS 入库，队列申请按历史峰值加裕量，不让 OOM 伪装成 segfault。
- 大设计默认 hyper-scale：超过规模阈值的设计直接走层次化验证流程，不做全平铺硬扛。
- svf 同代配套：综合、fm_shell、svf 三件套版本同代生成同代使用，跨大版本一律重新生成。
- include 树定期查环：工程级脚本周期展开 include 依赖，循环引用在 review 阶段拦截，不进跑批。
- 崩溃证据包模板化：core 的 bt、log 尾部、最小化用例、版本与环境快照四件套固定格式，上报厂商与内部复盘都省事。
这一篇在知识体系里的位置
本篇是 EDA 排错速查簇中「Formality 工具崩溃」节点的 FAQ 页。通用的段错误与 core 分析见 core dump 分析；Formality 正常流程见 形式验证与 LEC 流程，Formality 其他高频问题见 Formality 版本不匹配；同类工具的崩溃与资源问题见 SpyGlass 段错误/崩溃、SpyGlass 资源超限。
一句话总结
Formality 段错误先用「退出码 + dmesg + core 是否生成」把 OOM 误杀（137）与真段错误（139）分开：137 走内存通道，量 set_top/match 峰值 RSS、上 hyper-scale 层次化验证降峰值；139 用 gdb 取栈回溯按阶段分流——read 期崩查递归宏与循环 include，match/verify 期崩靠「最小化用例 + 版本二分三次运行」判已知 bug；svf 引导文件与旧 session 跨版本复用是 Formality 特有的崩点，须同代配套、清 session 重建；最后靠 core 默认保留、内存峰值建档、崩溃证据包模板化，让每次崩溃都留下可复盘、可上报的现场。