极客工场

Appearance

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

Formality license 获取失败怎么办：Unable to checkout 排错速查 ​

更新时间：2026-10-22。FAQ 速查页，属于 EDA 工具排错系列，总入口见 EDA 开源与报错索引。Formality（fm_shell / formality，Synopsys 形式验证工具）启动时第一件事是向 license server 签到（checkout），签到失败就直接退出，等价性检查一步都跑不了。Synopsys 全家桶的授权体系叫 SCL（Synopsys Common Licensing），底层是 FlexNet Publisher 那套 lmgrd 加 vendor daemon 架构，vendor daemon 换成 Synopsys 的 snpslmd，客户端优先读的变量是 SNPSLMD_LICENSE_FILE，通用 LM_LICENSE_FILE 只是兜底；DC、VCS、Formality 通常共用同一组 SCL 守护进程。本篇以 Formality 启动日志里的典型报错为锚，把「连不上、feature 版本不认或过期、席位占满」三类失效点逐条拆开。Formality 签到通过之后的用法见 形式验证（二）：LEC/Formality，工具内部报错可对照 Formality 模块找不到速查。

本文要回答的问题 ​

  • fm_shell 启动报 Unable to checkout a license / FlexNet -15，先查哪里？
  • SNPSLMD_LICENSE_FILE 和 LM_LICENSE_FILE 都设了，Formality 到底听谁的？
  • 服务器活着，为什么报 Licensed number of users already reached（-4），或者 feature 不存在、版本不支持（-5 / -21）？
  • Formality 的 feature 名到底叫什么，基本包和高级选项 add-on 签的是同一张 license 吗？
  • license 被异常退出的 fm_shell 会话挂住不释放，怎么确认和回收？

一、报错原文与典型现象 ​

Formality 的 license 报错通常出现在启动 banner 之后、命令行提示符出现之前，文案以 Unable to checkout 开头并附 FlexNet 负数错误码。以下为典型形态，服务器名一律占位：

1. 连不上 license server（启动即死，最常见）：

text
Unable to checkout a license for Formality.
Cannot connect to license server system.
  License path: 27000@<server>
  FlexNet Licensing error: -15,570.  System Error: 115 "Operation now in progress"

2. 服务器活着，但不认这个 feature 或版本：

text
Unable to checkout a license.
  Feature:          Formality
  FlexNet Licensing error: -21,126 "License file does not support this version."
text
Unable to checkout add-on license "Formality_Advanced".
  FlexNet Licensing error: -5,357 "No such feature exists."

3. license 到期（常见于年度维护合同续期没做完）：

text
Feature has expired.
  Feature: Formality
  Expiration date: 30-sep-2026
  FlexNet Licensing error: -10,32

4. 席位占满，排队或直接被拒：

text
Licensed number of users already reached.
  Feature: Formality
Your request has been queued.  Queue position: 2
text
Unable to checkout a license for Formality.
  FlexNet Licensing error: -4,132

一句话根因：Formality 本身没坏，是客户端到 SCL license server 这条链路某一环断了。 先抓住报错里的负数错误码：-15/-96/-97 是连不上（变量指错、lmgrd 或 snpslmd 没起、防火墙拦端口），-5/-21/-10 是连上了但 feature 不存在、Formality 版本新于 license 支持期或 license 已过期，-4 与 queued 是 feature 没问题但席位被占满。错误码比前面的大段英文更有指向性。

二、报错 → 原因 → 处置速查表 ​

报错现象最常见原因一条命令确认处置
-15 cannot connectSNPSLMD_LICENSE_FILE 端口或主机写错echo $SNPSLMD_LICENSE_FILE改为 27000@<server>（端口以管理员通知为准）后重跑
-15 且变量看着对lmgrd 或 snpslmd 没在跑lmutil lmstat -a -c 27000@<server>联系管理员重启 SCL：lmgrd -c <license.dat> -l <log>
-15 且 lmgrd UP防火墙拦了 snpslmd vendor 端口nc -vz <server> 27000，再测 vendor 口license 文件写 VENDOR snpslmd port=<固定口>，两端口一起放行
-96/-97 server down服务器停机，或 SCL 版本旧于客户端lmutil lmstat -a -c ... 看 daemon 行重启服务；SCL/snpslmd 不得旧于 Formality 客户端
-5 No such feature只买了基本包，没买高级 add-on，或 feature 名不匹配lmutil lmstat -f Formality -c ...核对 INCREMENT 行，向 Synopsys 确认本单位套餐 feature 名
-21 version not supportedFormality 版本发布日期晚于 license 维护期对照 INCREMENT 行版本日期与工具发布日期回退 Formality 版本，或申请新的 increment 后 lmreread
-10 expiredlicense 到期未续lmutil lmstat -i Formality -c ...走续期，新文件到位后管理员 lmreread 重读
-4 / queued席位占满，含崩溃残留的僵尸占用lmutil lmstat -a -c ... | grep -i formality排队等释放，或管理员 lmremove 回收僵尸席位
交互能跑、回归脚本签不到非交互 shell 没 source SCL 环境作业里 env | grep -i LICENSE变量写进工程环境脚本，不依赖个人 .bashrc
DC/VCS 同时签不到三套件共用 SCL，守护进程整体挂了lmutil lmstat -a -c ...按 SCL 整体故障处理，重启影响全套件需协调

三、排查决策树 ​

按「变量 → 服务 → 端口 → feature 与席位」四环收敛，错误码直接替你选路：连不上的走前三环，连得上但拿不到的走第四环。

eda/ts-formality-license-checkout-fail.md D2 示意图

读这张图抓住一条主线：红色入口往下，三个蓝色判定逐级证明「找对地方、服务器活着、网络通」，灰色节点处理 feature 与席位，橙色是各层对应的修复，绿色是收敛验证。前三环解决 -15/-96/-97 的「路不通」，第四环解决 -5/-21/-10/-4 的「路通了货不对」。任何一步命中都在那一层修，修完直接回到绿色节点复验，不要同时改三处——否则下次复发时说不清是哪一处生效。

四、逐条排查展开 ​

第一步：确认变量在「启动 fm_shell 的那个 shell」里真的有值。 Formality 查找 license 的优先级是 SNPSLMD_LICENSE_FILE → LM_LICENSE_FILE，值可以是 端口@主机（浮动 license），也可以是 license 文件绝对路径。最常见的事故是管理员迁移了服务器，通用变量改了、SNPSLMD_LICENSE_FILE 还指着旧机器，而专用变量优先，于是白改：

bash
env | grep -iE "SNPSLMD|LM_LICENSE|LICENSE"
# SNPSLMD_LICENSE_FILE=27000@<server>   ← 与管理员给的主机/端口逐字符对

交互终端里有值、LSF/cron/回归脚本里没有，几乎都是非交互 shell 不加载 .bashrc。把变量写进工程自己的环境脚本并在作业开头显式 source，不要假设调度系统继承桌面环境。

第二步：用 lmstat 看「双 UP」。 SCL 安装目录（$SCL_HOME/linux64/bin 下的 lmutil）自带查询命令：

bash
lmutil lmstat -a -c 27000@<server>
# 健康输出的两行关键状态：
#   <server>: license server UP (MASTER) v11.19
#     snpslmd: UP v11.19

lmgrd UP 和 snpslmd UP 缺一不可：只有 lmgrd 活着、snpslmd 没起来时，握手能开始但 checkout 必败，客户端照样报 -15/-96。DC、VCS、Formality 共用这一组守护进程，snpslmd 挂掉时三套件会同时签不到，这个现象反过来也能帮你确认是 SCL 整体故障而不是 Formality 单机问题。管理员换了 license 文件后需要执行 lmutil lmreread -c 27000@<server> 让 daemon 重读，只换文件不重读，新 feature 不会生效；lmdown 会踢掉所有在线用户，只能由管理员在维护窗口操作。

第三步：测两个端口，别只测 lmgrd 的口。 FlexNet 通信用两个端口：license 文件 SERVER 行上的固定端口（Synopsys 站点常用 27000，以实际文件为准）和 snpslmd 的 vendor 端口，后者默认每次启动随机分配。防火墙只放行了固定端口时现象很有迷惑性：lmstat 偶尔能应答，Formality 真正 checkout 时超时报 -15：

bash
nc -vz <server> 27000
lmutil lmstat -a -c 27000@<server> | grep -i "port"   # 找 snpslmd 实际端口后再 nc 一次

根治办法是让管理员在 license 文件里写 VENDOR snpslmd port=<固定端口> 钉死，防火墙把两个端口一起放行。若站点配三机冗余（triad），变量形如 27000@host1:27000@host2:27000@host3，多数存活即可签到，排查时逐个 nc。

第四步：-5/-21/-10——连上了但货不对。 三种成因分开看。-5 是 feature 不存在：Formality 签的是独立 feature（常见基本包 feature 名即 Formality，某些高级能力如复杂时序/低功耗相关选项以单独的 add-on feature 签出，具体名以本单位 license 文件 INCREMENT 行为准），只买了基本包却触发高级选项时就会在对应阶段报 add-on 签不出，用 lmutil lmstat -f <feature名> 确认服务器上到底有没有。-21 是版本不支持：INCREMENT 行上的日期表示「支持该日期之前发布的工具」，装了比它更新的 Formality 就会被拒——工具升级前必须先确认 license 维护合同与 increment 到位，否则就是全员停工。-10 是到期，lmutil lmstat -i Formality -c 27000@<server> 能直接看到到期日。另外 SCL/snpslmd 服务端太旧、Formality 客户端太新也会签到失败，服务端版本需不旧于客户端，这条要管理员在服务侧核对。

第五步：-4 与 queued——席位满员。 lmutil lmstat -a 能看到每个席位被谁、从哪台机器、从几点占用。两种处置：排队等释放（席位空出后按队列位置自动重试，位置提示即来自这里），或请管理员用 lmutil lmremove 清掉异常退出残留的僵尸会话——被 kill -9 的 fm_shell 心跳超时前不会立刻还席。同一组 license 被 DC、VCS 作业挤占时也要按全套件视角协调，不要只盯 Formality 的计数。

第六步：每改一处立刻复验一次。 先空壳签到（fm_shell -x quit 起来即退），确认无 license 报错；再跑一个最小 LEC 流程完整走一遍 setup-match-verify——add-on feature 可能在运行到对应阶段才签出，启动能过不代表全程能过。两级都绿才算闭环。

五、预防与纪律 ​

  • 变量进工程脚本：SNPSLMD_LICENSE_FILE 写进团队统一环境 setup，回归作业开头 source 并打印一行确认，不靠个人 .bashrc。
  • 升级先查维护期：Formality 大版本升级前，用 INCREMENT 行日期对安装包发布日期，同时确认 SCL 服务端版本，license 没到位不全网推送。
  • vendor 端口钉死：新装机或迁移服务器时，license 文件直接写 VENDOR snpslmd port=<固定口>，避免动态端口与防火墙长期扯皮。
  • 续期看日历：记下 license 到期日，提前两周走续期流程，不要等 -10 在流片前夜出现。
  • 报错原文先存档：保留第一次失败的完整启动日志，改一处重跑一次；报错行自带错误码与 license path，原文即证据。

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

本篇是 EDA 排错速查簇的一员，总入口见 开源 EDA 报错排错中心。Formality 签到通过之后的完整流程见 形式验证（二）：LEC/Formality，验证域概念背景见 验证域 LEC；工具内部读入与匹配阶段的报错对照 Formality 模块找不到速查，Mentor 侧（MGLS/mgcld）的同款签到故障可对照 Calibre license 获取失败速查，两篇 FlexNet 错误码语义通用，差异只在 vendor daemon 与专用环境变量。

一句话总结 ​

Formality license 获取失败，本质是 Formality 经 SCL（FlexNet 架构、vendor daemon 为 snpslmd、优先读 SNPSLMD_LICENSE_FILE，与 DC/VCS 共用守护进程）签到失败：按错误码分流——-15/-96/-97 依次核对变量主机端口、lmutil lmstat -a 看 lmgrd 与 snpslmd 双 UP、nc 验固定端口与 vendor 两个端口；-5/-21/-10/-4 分别对应 feature 名或套餐不符、Formality 版本超出 license 维护期、license 到期、席位占满排队，用 lmstat -f/-i 定位，配合 lmreread 重读、lmremove 回收僵尸席位；修完以 fm_shell 空跑签到加最小 LEC 流程完整跑通为验证标准，防复发靠变量进工程脚本、升级前核对维护期、vendor 端口钉死三件事。