Formality 运行卡死/超时：fm_shell hang 住不动排查速查
更新时间：2026-10-23。FAQ 速查页，属于 EDA 工具排错系列。Formality 的「卡死」同样分两种气质：一种是真在算（verify 阶段遇到乘法器、大位宽除法这类组合逻辑，求解器病态展开，CPU 单核打满几十小时不稀奇），一种是真挂了（等 license 队列、交互模式忘加 -f 脚本干等 stdin、stdout 管道没人读）。第一步永远是分清这两种——杀错一个跑了九成的 verify 任务，整晚的机器时间就白烧了。进程直接崩掉（段错误、信号退出）的另一条线见 Formality 段错误崩溃排查，license 显式 checkout 报错见 Formality license 拉取失败。
本文要回答的问题
- fm_shell 起跑后几小时没结果，transcript 停在一行不动，是死了还是在算？
- verify 在什么设计上会组合逻辑爆炸，怎么先出粗结果？
- 等 license 队列的 hang 为什么不报任何错？
- 交互模式忘加 -f、管道阻塞、swap 颠簸各是什么形态？
一、报错原文与现象
（无报错——transcript 最后一条停在三小时前）
Info: Matching compare points in reference design 'WORK.top' ...
Matched: 81234 compare points (81200 by name)
（进程还在，CPU 0%，时间戳不再更新）卡死类问题「没有报错」就是报错本身。先锚定三个现场：transcript 最后一条停在哪、进程还在不在、CPU 是 0% 还是 100%——这两个极端形态直接把病因分成「等外部事件」和「在病态电路上空转」两大阵营。
二、可能原因总览
| 现象特征 | 可能原因 | 处置 |
|---|---|---|
| 日志停在 license checkout 前一行、CPU 0% | FlexLM 令牌占满，静默排队不报错 | lmstat 查池、释放僵死会话或错峰 |
| verify 阶段 CPU 单核 100%、日志龟速推进 | 乘法器/大位宽除法等组合逻辑病态展开 | 降 effort、设 verification_timeout、拆区域 |
| 日志停在 match 阶段、无新输出 | 命名规则失配导致匹配搜索空间爆炸 | 调 name_match 策略、查未匹配点分布 |
| 裸跑 fm_shell 无 -f，终端停在提示符 | 交互模式干等 stdin 输入 | 批处理统一 fm_shell -f run.tcl |
| 直接跑正常、走管道就 hang | stdout 接到没读者的 pipe，缓冲写满 | 改重定向到文件、分段落盘 |
| CPU 低、负载高、内存吃满未 OOM | 超大扁平设计 swap 颠簸 | 加内存、hyper-scale 分层验证 |
| 单个 hard verification 区域永远跑不完 | 局部病态逻辑锥 | set_dont_verify 隔离后单独攻关 |
| RUNLIMIT 被调度系统杀掉 | 时限按小设计估的 | 按分段日志校准 p95 时限 |
三、逐条排查展开
第一刀：top + /proc 给 fm_shell 把脉。
top -b -n1 | grep -E "fm_shell|formality"
tail -5 formality.log
cat /proc/<pid>/status | grep -E "State|VmRSS"CPU 持续单核 100% 是真在算阵营；CPU 近 0% 是等外部事件阵营；State 是 D（不可中断睡眠）则进入 IO/NFS 线。别拿单次采样下结论，连采三次。VmRSS 逼近物理内存、整机变卡，是 swap 颠簸的形态。
等 license 的 hang 最阴险：排队等待不报错。 Formality 令牌被占满时，fm_shell 安静地停在 checkout 前，没有 Waiting 字样、没有超时、没有重试——transcript 看起来就是「正常启动到一半停了」。判别：进程 S 态、CPU 0%、日志停在启动早期。用 lmstat 看池子：
lmstat -a -c <port>@<license-server> | grep -i formality占着令牌的多半是挂了没退干净的会话。处置不是重启（重启只会重新排队），而是让管理员释放僵死会话或错峰调度。与「静默排队」不同，checkout 直接报错的处理见 Formality license 拉取失败。
verify 组合爆炸是 Formality 特有的「真在算但等于死了」。 verify 要把 reference 与 implementation 的每个 compare point 证明等价，遇到乘法器、大位宽除法、桶形移位器这类算术逻辑，SAT/BDD 求解器会病态展开——CPU 单核打满，跑几十小时不出结果，与 hang 唯一区别就是 CPU 占用。判别：strace -c -p <pid> 看是密集计算而不是卡在 syscall；transcript 里 Verifying ... 进度长时间停在同一片逻辑。处置三板斧：先 set verification_timeout 4:00:00 给单次验证封顶，超时按 inconclusive 收场而不是无限烧；set verification_effort_level low（或 set_verify effort low 老语法）先出粗结果，确认大面积等价后再针对难点区域加 effort；对确认无害的病态区域用 set_dont_verify 隔离，单独攻关。长期方案是 hyper-scale 分层验证——子模块先各自等价，顶层只做接口比对，把组合爆炸挡在模块边界内。
match 阶段长时间无输出是另一条「在算」线。 日志停在 Matching compare points ... 之后不再推进，多半是综合后网表命名被工具改得面目全非，name-based 匹配大面积落空，Formality 退到基于功能的匹配搜索，空间爆炸。判别：report_matched_points 与 report_unmatched_points（若能另开一会话 attach 同库）看未匹配比例；命名规则混乱是信号。处置：调 set name_match ... 系列策略放宽匹配方式，或在综合侧开 set_app_var formality ... 写出指导文件（svf），让匹配走指导而不是盲搜。
交互模式干等 stdin 专咬「调度脚本抄了手工命令」的人。 提交脚本写成裸 fm_shell 没带 -f run.tcl，进程正常起来了，停在 fm_shell> 提示符等键盘输入——而批处理节点根本没有终端连着它。CPU 0%、transcript 停在 banner 之后、进程状态 S，是这个病的三联征。根治：批处理入口统一封装为 fm_shell -f run.tcl -output_log_file formality.log，禁止裸起交互进程进回归。
管道阻塞与 swap 颠簸是尾部两类「像死了」。 fm_shell ... | tee log 下游读者退出后缓冲写满，进程阻塞在 write，改成重定向到文件就正常——日志分段落盘最稳。超大扁平设计内存需求超物理内存时不 OOM 但 swap 颠簸：系统负载飙高、CPU 利用率反而低、全程慢得像死了，free -g 看 swap 用量即可确诊，处置是换大内存机器或上 hyper-scale 分层。
下图把上面的分流逻辑画成一张决策图。
颜色按语义分角色：红是卡死入口与三种确认的病态形态，蓝是排查动作，绿是「确诊 verify/match 病态展开」这条「真在算但需干预」的分支，橙是修复动作，紫是收尾防复发。主线是「把脉三件套先按 CPU 与进程状态分阵营：打满的再按 match/verify 分线，近零的按日志最后一行分流」——license、stdin、管道、swap、NFS 各占一条，互不串味。
四、预防与纪律
- 分段日志打时间戳：read / elaborate / match / verify 每段头尾各打一行 transcript，hang 了最后一行就是定位锚点。
- 批处理一律 fm_shell -f 封装：从提交脚本层消灭「裸起交互进程干等 stdin」这个病，禁止交互命令混进回归。
- verification_timeout 必设：每次 verify 封顶数小时，超时按 inconclusive 收场进人工队列，不许无限烧机器。
- svf 指导文件全程开：综合侧落 svf，match 走指导不盲搜，从源头压掉匹配搜索空间。
- 大设计上 hyper-scale 分层：子模块先行等价，顶层只做接口比对，组合爆炸挡在模块边界内。
- 时限按历史 p95 校准：每个设计分段建档耗时，RUNLIMIT 取 p95 的 1.5 倍，超时先收日志再杀。
- 令牌占用例行公示：谁占着 Formality 令牌一目了然，排队纠纷当天解决。
这一篇在知识体系里的位置
本篇是 EDA 排错速查簇中「Formality 运行态卡死」节点的 FAQ 页，与 SpyGlass 运行卡死/超时 同构互参（把脉三件套与分流逻辑通用）；进程崩溃而非挂起的线见 Formality 段错误崩溃排查；license 显式报错的线见 Formality license 拉取失败；Formality 等价验证流程背景见 形式验证与 Formality LEC 流程。
一句话总结
Formality 卡死先用「CPU + 进程状态 + 日志最后一行」三件套分阵营：CPU 打满再分 match/verify——verify 病态展开靠 verification_timeout 封顶、降 effort、set_dont_verify 隔离，match 盲搜靠放宽 name_match 加 svf 指导；CPU 近零按日志分流——停在 checkout 前查 FlexLM 令牌池、停在 banner 后是忘加 -f 干等 stdin、走管道才复现改分段落盘、负载高内存满查 swap；D 态杀不掉一律查 IO/NFS。长期靠分段日志、-f 封装、svf 指导、hyper-scale 分层与时限校准五件套，让每次 hang 都能当场定位。