极客工场

Appearance

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

Formality 版本不匹配怎么办：fm_shell 版本报错速查 ​

更新时间：2026-10-22。FAQ 速查页，属于 EDA 工具排错系列，总入口见 EDA 开源与报错索引。Formality（fm_shell / formality，Synopsys 形式验证工具）的版本问题有四副面孔：启动的 fm_shell 不是你以为的那一套、旧会话恢复时容器数据库读不回来、综合引导文件 SVF 与工具大版本对不上、license 维护期不覆盖当前版本。它们都吐「version」字样，但断点分别在环境、数据、配对、授权四处，处置完全不同。Formality 的完整 setup-match-verify 流程见 形式验证（二）：LEC/Formality，验证域背景见 验证域 LEC；若报错只停在签到阶段，先看姊妹篇 Formality license 获取失败速查。

本文要回答的问题 ​

  • incompatible database version 和 cannot restore session 是文件坏了还是版本不对？
  • 明明 module 加载了新版，为什么 which fm_shell 还指向老安装？
  • DC 综合出的 SVF guidance 在 Formality 里大量 ignored，与版本有什么关系？
  • version not covered by license / FlexNet -21 是装错了还是授权过期？
  • 为什么版本切换后统一要求「从头 setup」，不能接着上次的 session 跑？

一、报错原文与现象 ​

1. 恢复旧会话时容器数据库被拒读（最典型）：

text
Error: Cannot restore session 'runs/fm_session'.
  The session database was created by a newer version of Formality
  (<version-newer>) and cannot be read by version <version-older>.
  (FMR-...)

2. 读入 .fsv 容器数据或 save_session 产物时格式不兼容：

bash
Error: Incompatible database version while reading container database
  file './work/fm_shell_cmd.<...>.fsv'.
Warning: Session directory './work/fm_session' was written by
  Formality <version>; its format is not compatible with this release.

3. SVF guidance 与综合工具版本不配对：

text
Warning: The guidance file 'top.svf' was generated by Design Compiler
  <version-dc>. Some guidance items are not recognized by this
  Formality <version-fm> and will be ignored.
Information: 37 guidance items accepted, 41 ignored.

4. 签到通过前就被挡下，版本不被 license 覆盖：

text
Unable to checkout a license for Formality.
  Feature: Formality
  FlexNet Licensing error: -21,126 "License file does not support this version."

前两类断在 restore/读数据阶段，是数据与工具的版本绑定问题；第三类断在 match 引导阶段，是 DC 与 Formality 的发布批次配对问题——ignored 项一多，retime/常量传播导致的比较点失配就无人引导，验证直接跑不动；第四类断在启动签到，是授权维护期问题，错误码语义与 license 篇完全一致。另有一类无报错的隐形式混版：which fm_shell 指向的二进制和 module list 显示的根本不是同一套安装，现象是同一工程「换人跑就挂」。

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

报错现象最常见原因一条命令确认处置
Cannot restore session / newer version会话由更新版 Formality 保存看报错里两侧 <version>弃用旧 session，从 RTL/网表从头 setup
Incompatible database version 读 .fsv容器数据库跨大版本不兼容查 work/ 目录由哪版生成删旧工作目录重跑，不迁移 .fsv
guidance items ignored 过半SVF 由不配对的 DC 版本写出对 DC banner 与 Formality 大版本DC/FM 同批次配对，重综合重出 SVF
-21 does not support this version工具发布日期晚于 license 维护期lmutil lmstat -i Formality回退工具版本或申请新 increment
交互正常、回归脚本报版本错脚本里硬编码老安装路径grep -n "synopsys" run.tcl路径改为变量，统一由环境脚本提供
module 已加载新版仍跑老版PATH 中老路径排在前面which -a fm_shell调整 PATH 顺序或卸掉个人软链
FORMALITY_HOME 与 SYNOPSYS 互串两套工具变量被同一 setup 污染`env | grep -iE "FORMALITYSYNOPSYS"`
极老库/会话报位数错误32 位老安装读 64 位数据（或反之）看安装目录 linux 还是 linux64统一用 64 位当前版本，老数据重建
升级后所有人结果不一致升级只装包、没定版没清工作区各人 fm_shell -version 对一遍统一 module 定版，清 work 后重跑基线

三、逐条排查展开 ​

先抄两个版本号：工具侧与数据侧。 工具侧看启动 banner，或在 shell 里直接查：

bash
fm_shell -version
which -a fm_shell
echo $FORMALITY_HOME
module list 2>&1 | grep -iE "formality|synopsys"

fm_shell -version 给真实版本，which -a 列出 PATH 上所有同名二进制——两者一对，安装串台立刻现形。数据侧版本报错信息里直接给出（<version-newer> 对 <version-older>），先判谁比谁新，再决定走哪条修复路，不要一上来就重装。

安装串台：PATH、硬编码路径与工具变量三处查。 多套 Synopsys 安装并存的机器上，串台通常来自三处：个人 .bashrc 里把老路径加在 PATH 前面；回归脚本里写死了 /tools/synopsys/formality/<version>/bin 一类绝对路径；FORMALITY_HOME 与 DC 的 SYNOPSYS 变量被同一份 setup 脚本交叉覆盖，启动器按变量找到老安装。排查时在真正跑作业的那个 shell（LSF/cron 的非交互环境尤其要重新确认）里执行上面四条命令，任何一条与团队定版不符就在环境层修，而不是在工程脚本里迁就。

会话与 .fsv：不做跨版本迁移，一律从头 setup。 Formality 的 session（save_session 产物，含 .fsv 容器数据库）是二进制序列化状态，格式与大版本绑定，策略与 DC 的 ddc 一样——宁可拒读，不可错读。看到 cannot restore session 不要尝试「转换会话」，正路是删掉旧工作目录，从源重新走一遍：reference 侧读 RTL、implementation 侧读网表与库，重新 set_top、match。本来就应该交接 RTL/网表 + SVF，而不是交接 session 目录；session 只作同一版本内断点续跑用。

SVF 配对：DC 与 Formality 必须同批升级。 SVF 是 DC 综合时（set_svf 打开后）写出的引导文件，记录 retime、常量传播、重命名等变换，供 Formality 在 match 阶段把比较点拉回对应关系。SVF 的引导语义随发布批次演进，Formality 不认的条目直接 ignored——accepted 与 ignored 计数会在日志里列出。配对原则是用同一年度发布批次的 DC 与 Formality，升 DC 必须连 Formality 一起升；版本错位时不要手工修 SVF，让配对后的 DC 重新综合、重新出 SVF，再从 setup 跑起。

license 维护期：-21 是授权问题不是安装问题。 INCREMENT 行日期只支持该日期之前发布的工具，装了更新版 Formality 就报 License file does not support this version。处置二选一：回退到维护期内的版本，或等管理员续期拿到新 increment 后 lmreread。完整的错误码语义、lmstat -i 查到期日、SCL 服务端版本不得旧于客户端等排查动作，按 Formality license 获取失败速查 走，本篇不重复。

eda/ts-formality-version-mismatch.md D2 示意图

读这张图抓住一条主线：红色入口只做一件事——抄版本号；蓝色判定之后按报错措辞四选一，橙色四条修复路径分别对应环境、数据、配对、授权，最后全部汇到绿色收敛点。任何一步命中就在那一层修，修完直接回到「统一环境后全流程重跑」复验，不要环境、数据、license 同时改，否则复发时分不清是哪一处生效。注意四条路径的成本不同：换 module 是分钟级，从头 setup 是小时级，续期要等管理员，能在报错文案里直接分流就不要逐条试。

四、预防与纪律 ​

  • DC 与 Formality 成对定版：项目启动时在工程环境脚本（modulefile 或 project.env）里写死同一发布批次的两个版本，所有人与 CI 同源 source，禁止个人 .bashrc 另加路径。
  • 会话不跨版本、不入版本库：work/、*.fsv、session 目录都是可再生中间产物，进忽略清单；断点续跑只在同一版本内使用，升级即清空。
  • 交接只交源：跨团队交接给 RTL、门级网表、SDC 与配对 DC 产出的 SVF，不交 session 与容器数据库。
  • 升级走窗口：升 Formality 先确认 license 维护期与 SCL 服务端版本覆盖新发布日期，再连 DC 同批切换，切换后清工作区全量重跑作为新基线。
  • 脚本禁绝硬编码路径：安装路径一律取自 FORMALITY_HOME 等变量或 module 提供的路径，机器迁移安装目录时工程脚本零修改。

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

本篇是 EDA 排错速查簇的一员，总入口见 开源 EDA 报错排错中心。版本问题解决后，Formality 的标准验证流程与 setup-match-verify 各阶段含义见 形式验证（二）：LEC/Formality，为什么要做逻辑等价性检查见 验证域 LEC；报 -15/-4/-5 等签到错误时按 Formality license 获取失败速查 处理，综合侧 DC 的库与 ddc 版本问题则是同一「数据格式绑定工具版本」原则在另一工具上的表现。

一句话总结 ​

Formality 版本不匹配先从报错抄下工具侧与数据侧两个版本号，再按措辞四分流：which -a fm_shell 与 FORMALITY_HOME 查实安装串台的，回到 module 定版、删掉硬编码路径；报 incompatible database version / cannot restore session 的，弃用旧 session 与 .fsv，从 RTL、网表和配对 SVF 从头 setup；SVF guidance 大量 ignored 的，按同一年度发布批次让 DC 与 Formality 成对升级、重新综合出 SVF；报 -21 not covered by license 的回退版本或走续期；根治靠工程环境统一脚本定版、会话不跨版本不入库、升级先查 license 维护期三件事。