极客工场

Appearance

共 2,403 字预计阅读约 8 分钟

Formality 资源/内存超限：verify 被 OOM 杀掉速查 ​

更新时间：2026-10-23。FAQ 速查页，属于 EDA 工具排错系列。Formality（fm_shell）做大规模 LEC 等价性检查时，资源被打爆是仅次于 license 的高频故障：setup 阶段读入两个设计的网表就要吃掉一大块内存，match 阶段建立对应点映射再翻一倍，verify 阶段的 cone 比较才是大头。这类问题的麻烦在于报错形态分散——有时是工具自己报 out of memory，有时是 shell 只留一句 Killed，有时是进程没死但慢得像死了（swap 颠簸）。本篇与 Formality 运行卡死/超时 分工：那篇是「逻辑上比不完」（effort level、难解 cone），这篇是「机器资源先扛不住」；进程猝死的另一条线见 Formality 段错误崩溃。

本文要回答的问题 ​

  • fm_shell 跑着 verify 突然没了，日志停在一半，是谁杀的？
  • out of memory 是设计太大，还是 parallel 线程开太多？
  • 物理内存明明还有剩，为什么还是申请失败？
  • 不换大内存机器，怎么用 hyper-scale 把大设计拆小跑完？

一、报错原文与现象 ​

text
Error: out of memory (FM-055)
fm_shell: memory allocation failed, requested 8589934592 bytes
Killed                              （shell 层一句话，fm_shell 日志戛然而止）
bsub: JOB 9527 TERM_MEMLIMIT: memory limit reached
Warning: verification incomplete due to insufficient resources (FM-081)

先建立映射：out of memory / memory allocation failed 是 fm_shell 自己申请内存失败（撞 ulimit 或物理耗尽）；Killed 无工具报错则是内核 OOM killer 动的手；TERM_MEMLIMIT 是 LSF 调度层的配额杀；verification incomplete due to insufficient resources 最阴——工具没死但主动放弃了部分 cone，结果不可信，必须当失败处理。五种形态对应五条排查线，别混。

二、可能原因总览 ​

报错现象可能原因处置
Killed、日志戛然而止OOM killer 按峰值 RSS 杀进程dmesg 确认，降峰值或换大机
out of memory（FM-055）峰值内存超物理 RAM 或 ulimit -v看 VmPeak 量峰值，调限制或降压
verification incomplete（FM-081）内部资源预算耗尽主动放弃降 verification_effort_level 后拆跑
TERM_MEMLIMIT 被杀bsub 内存限额估小按历史峰值重设 -M/-R
match 阶段爆内存两设计对应点映射表过大加 guidance（SVF），拆层次
verify 阶段爆内存cone 比较组合爆炸、effort 过高降 effort level，hyper-scale 拆分
parallel 多线程互挤每 worker 各吃一份设计数据降 set_host_options 的 max_cores
启动即失败或深层递归死ulimit -s/-v 太小、32 位模式调栈上限，确认 64 位 fm_shell

三、排查决策图 ​

排查主线是「报错字样直接决定第一查」：红色是报错入口与命中根因，蓝色是排查动作，橙色是修复，紫色是收尾防复发。Killed 找 dmesg、自报 OOM 量 VmPeak、incomplete 降 effort、MEMLIMIT 找历史峰值——四条线最终都收敛到「降并发/拆规模 → guidance 辅助 → 调度预留」三级修复。

eda/ts-formality-resource-overflow.md D2 示意图

这张图读法：从顶部红色入口往下，先在蓝色分流节点按日志里的字样选对岔路，再到蓝色排查节点拿到实锤（dmesg 记录或 VmPeak 数值），命中的根因标红，对应橙色修复动作，最后全部汇入紫色防复发节点。注意左右两条主线的修复手段不同——左线是「拆设计规模」，右线是「给工具更多辅助信息」，顺序是先辅助后拆分，因为加载 guidance 几乎零成本。

四、逐条排查展开 ​

进程凭空消失，先问内核要口供。 Linux 内存耗尽时 OOM killer 挑最占内存的进程杀，被杀者收不到任何错误码——fm_shell 日志戛然而止，shell 只留一句 Killed。口供在内核日志里：

bash
dmesg -T | grep -iE "out of memory|oom|killed process" | tail -5

看到 Out of memory: Killed process xxxx (fm_shell) 就实锤了。如果 dmesg 里留的是 segfault at 而不是 oom 字样，那是另一条线，判别与处置见 Formality 段错误崩溃。

峰值内存到底涨了多少，看 VmPeak。 别凭感觉判断「机器不够」。fm_shell 运行中可以随时查它的内存高水位：

bash
grep VmPeak /proc/$(pgrep -f fm_shell | head -1)/status

VmPeak 是进程历史峰值虚拟内存，VmRSS 是当前常驻。跑完后想复盘，用 /usr/bin/time -v fm_shell -f run.tcl 重跑一次，日志末尾的 Maximum resident set size 就是峰值 RSS。拿到峰值后对照三样东西：机器物理 RAM、bsub 限额（有的话）、ulimit -v——谁最小谁就是瓶颈。经验值：百万门级设计 setup 阶段吃掉十几 GB 常见，verify 阶段 cone 比较再翻数倍。

parallel 线程不是白来的，每个 worker 各吃一份内存。 set_host_options -max_cores 8 让 verify 并行，但工作进程各自加载设计数据，内存近似按核数上涨。内存紧张时第一刀就是降 max_cores：8 核跑 2 小时被杀，不如 2 核跑 6 小时跑完。同机多作业互挤同理——别人也在同一台机器上跑 fm_shell 时，调度侧用 bsub -R "rusage[mem=64G]" 按内存预留，从源头消灭互挤型 OOM。

effort level 与 incomplete 的关系要懂。 set verification_effort_level high 让工具在难 cone 上砸更多求解资源，内存与时间同步暴涨；资源预算耗尽时工具报 verification incomplete（FM-081）主动放弃——这种结果不能当通过，签名审核时必须拦下。处置顺序：先用默认（medium）跑一遍看哪些 cone 失败，只对小范围失败点局部提 effort，而不是全设计 high。

match 阶段爆内存，多半是缺 guidance。 Formality 靠 SVF（setup verification for Formality）文件知道综合工具做了哪些优化（寄存器合并、重命名、ungroup），没有 SVF 时 match 阶段要自己猜对应关系，映射表暴涨。处置是把综合流程输出的 SVF 用 set_svf 加载进来——这一步经常直接把 match 峰值砍掉一半以上，比换机器便宜得多。

ulimit 与 32 位遗留问题。 老流程脚本如果走了 32 位 fm_shell，单进程地址空间上限约 4 GB，大设计必撞内存失败——哪怕机器有 128 GB 也救不了，确认启动日志里是 64 位模式。ulimit -a 顺手看 -s（栈）与 -v（虚拟内存）：深层 Tcl 递归会先撞栈上限，官方环境一般要求 ulimit -s unlimited。bsub 作业继承提交时的 ulimit，要改就写进提交封装脚本。

「以前能跑、最近开始爆」先对比再加资源。 同一设计历史上跑得动、最近开始 OOM，变量出在输入侧：设计规模涨了、SVF 丢了或没更新、effort level 被人调高、工具升了版本（如 2025.06 之后默认检查项变化）。把上次成功 run 的日志翻出来对比各阶段内存报告行，峰值涨在哪一阶段，压力就源于哪一阶段。盲目换大内存机器可能掩盖一个本该被发现的流程回归。

全芯片 verify 吃不下就上 hyper-scale。 hyper-scale 是 Formality 官方的分层验证方案：block 级各自完成 LEC 后，顶层用 block 的验证结论做抽象拼装，峰值内存按最大 block 算而不是全芯片。这是大项目存活的基本功——别等全芯片 verify 跑爆再返工拆。配套手段是增量策略：只重跑 ECO 改动波及的 block 与对应 cone，失败重跑也只重跑失败那一段。

五、预防与纪律 ​

  • 每个项目建峰值档案：用 time -v 或 VmPeak 记录 setup/match/verify 各阶段峰值，bsub 限额按峰值 1.3 倍配置。
  • max_cores 按机器内存反推上限：单核峰值乘以核数留 20% 余量，不许拍脑袋开满。
  • SVF 随网表一起交付：综合出网表时同步出 SVF，版本错配的 SVF 比没有更危险。
  • ulimit 写进作业封装：-s unlimited、64 位模式在提交脚本里固化，不依赖交互环境。
  • 大设计从立项就走 hyper-scale：block 级签核加顶层抽象拼装，别等全芯片跑爆再拆。
  • incomplete 一律当失败：FM-081 出现在日志里就阻断签核流程，不许人工放行。

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

本篇是 EDA 排错速查簇中 Formality「资源配额」节点的 FAQ 页。同簇互参：进程「比不完」类见 Formality 运行卡死/超时（effort level 与难解 cone 的取舍在那边展开）；进程「猝死」的另一条线见 Formality 段错误崩溃；同主题在另一工具上的对照见 SpyGlass 内存超限（lint/CDC 场景的峰值治理思路互通）。

一句话总结 ​

Formality 资源超限按报错字样分流：Killed 查 dmesg 的 OOM 口供、自报 out of memory 用 VmPeak 量峰值、FM-081 incomplete 降 effort 并局部重试、MEMLIMIT 按历史峰值重设；修复按「降 max_cores → 加载 SVF guidance → hyper-scale 分层拆跑」三级递进，长期靠峰值档案与 SVF 同步交付把内存问题从救火变规划。