极客工场

Appearance

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

Formality 缓存陈旧速查：改了 RTL 结果没变与 fm_shell 旧产物复用处置 ​

更新时间：2026-10-23。FAQ 速查页，面向在共享 Linux 服务器或容器环境里跑 Formality 形式验证（LEC）回归的同学。fm_shell 本身不缓存比对结论，但它的输入链路处处是「上次跑的产物」：svf 引导文件来自上一次综合、work 目录里躺着旧会话与中间库、恢复会话用的 .fms 保存点、容器镜像里复用的 .synopsys 配置缓存，再加 NFS 上时间戳漂几秒，任何一环把旧产物喂回来，现象都是同一句话——RTL 明明改了，比对报告却和昨天一模一样。这类问题没有报错弹窗，形式上是「跑通了」，危害比崩溃更大：回归全绿但验证对象根本不是当前代码。版本切换引起的另一类不兼容（缓存格式对不上）交叉参考 Formality 版本不匹配速查，产物写一半被判陈旧的鉴别见 Formality 文件损坏截断速查。

本文要回答的问题 ​

  • 改了 RTL 重跑 fm_shell，比对结果和上一轮完全相同，先怀疑哪一环？
  • set_svf 指到的 svf 是旧的综合产物，怎么确认与纠正？
  • work 目录里哪些残留会让 fm_shell 复用旧容器与中间库？
  • NFS 时间戳漂移为什么会让增量判断「看走眼」？
  • 先清缓存全量重跑验证、再定位缓存来源，这套方法论怎么落地？

一、典型现象与现场描述 ​

最常见的现场是回归脚本连跑两轮，第二轮改了 RTL，报告却逐字节一致：

bash
$ fm_shell -f run_fm.tcl | tee run2.log
...
Verification SUCCEEDED
  248 compare points matched, 0 failing
$ md5sum run1.log run2.log
9f2e1a...  run1.log
9f2e1a...  run2.log        # 时间戳以外完全一致

第二种现场在恢复会话阶段。fm_shell 从保存点或旧 work 目录恢复时给出提示，但回归脚本不检查这类 message，旧容器被悄悄用上：

text
Info: Restoring session from "/proj/fm/work/FM_CONTAINER"
Info: Using existing SVF setup from previous session
Warning: Reference design was read from saved container

第三种现场最隐蔽：svf 文件本身存在、格式也没问题，但它是上次综合跑的产物——综合脚本这次根本没重新生成它，set_svf 读到的是三天前的引导信息。Formality 不会替你核对 svf 的生日，照单全收。三种现场共同的判据是同一条：当前 RTL 的时间戳比比对报告里所有输入都新，结果却没变——看到这个组合，先把「陈旧」列为头号嫌疑，再谈别的。

二、陈旧来源与病因处置表 ​

陈旧来源典型位置现场特征处置
svf 未重新生成svf/ 目录或 set_svf 目标svf 时间戳早于本次综合综合成功后重生成 svf，比对前校验时间戳
work 目录残留FM_WORK、FM_CONTAINER恢复旧容器与中间库每轮独立 work 目录，跑前整目录清
会话保存点复用.fms / checkpointrestore_session 带回旧参考设计回归默认从零起跑，保存点只用于调试
容器内 .synopsys 缓存容器镜像家目录换镜像不换卷，旧配置被复用缓存卷按版本分目录，升级即换
NFS 时间戳漂移共享卷上的 rtl/svf文件内容变了、mtime 没变或倒退构建机与计算机对时（NTP），touch 强制刷新
版本切换缓存不兼容老版本留下的 work/缓存读旧格式缓存报怪错或静默复用升版本先全量清缓存，见 Formality 版本不匹配速查
依赖快照未更新文件清单/manifestrtl 清单还是旧一批文件每轮重生成依赖清单，比对前 diff 确认
写半截被判陈旧上一轮中断的 svf文件新但内容残缺按 Formality 文件损坏截断速查 处置，先整链重跑

表中「现场特征」一列用来在不清缓存的情况下先判断嫌疑方向；确诊仍然靠全量重跑这一步。

三、排查决策图 ​

陈旧问题的正确顺序是：先清缓存从零全量重跑一次确认「结果确实会变」，再回头逐环定位是谁喂了旧产物。顺序反了——先改这改那再重跑——会让多个变量混在一起，永远说不清哪个缓存是元凶。

eda/ts-formality-build-cache-stale.md D2 示意图

读这张图抓住主线：红色入口先接蓝色「清缓存全量重跑」这一步判定实验——它是全图唯一的关键动作，把「是不是缓存问题」变成一个有结论的对照实验。判定分叉后，绿色分支确认存在陈旧来源才进入逐环定位（仍是蓝色排查动作），橙色是命中环的修复，紫色闭环把修复固化进回归脚本防复发；另一条红色分支「清了还一样」说明病根在 RTL 输入本身（比如改的模块没被例化进比对层级），不在本篇范围。不要跳过判定实验直接逐环猜——七个嫌疑环挨个试一遍，比重跑一次贵得多。

四、逐条排查展开 ​

第一刀：清缓存全量重跑，先做对照实验。 在工作目录执行（路径以 /proj/fm 占位）：

bash
rm -rf /proj/fm/work/FM_CONTAINER /proj/fm/work/FM_WORK
rm -f /proj/fm/svf/default.svf          # 强制综合链重新生成
rm -rf ~/.synopsys_cache_2025_06        # 用户级缓存按版本分目录
fm_shell -f run_fm.tcl | tee rerun.log

清完从零跑一轮：结果随 RTL 变化，说明此前确有陈旧产物被喂进来，进入下一步定位；结果仍不变，先怀疑 RTL 改动根本没进比对层级（例化路径、宏开关、read_verilog 的文件清单），别再翻缓存。

第二刀：svf 生日校验，回归脚本必加的一行。 svf 是综合器写给 Formality 的引导文件，记录优化过程中的 retiming、ungroup 等操作，必须是本次综合的产物。回归脚本里在 set_svf 之前加校验：

bash
# 综合完成标志文件必须比 svf 新，否则说明 svf 是旧产物
test svf/default.svf -nt logs/synth.done || {
  echo "ERROR: svf older than synthesis run, regenerate first"; exit 1; }

fm_shell 侧读到旧 svf 不报错，但比对时按旧的优化映射对点名，结果要么假绿要么大面积 mismatch——先核对时间戳再谈比对结论。

第三刀：work 目录与会话保存点，回归和调试分两套玩法。 交互调试时恢复保存点省时间，回归批量跑必须每轮独立 work 目录、从零起读设计：

bash
WORK=/proj/fm/work/run_$(date +%Y%m%d_%H%M%S)
mkdir -p $WORK && cd $WORK
# run_fm.tcl 里不要出现 restore_session，回归默认全量起跑

如果脚本里为了「提速」复用了上一轮的 work 目录，fm_shell 会复用其中的容器与中间库，改动过的 RTL 即便重新 read，参考侧容器仍可能是旧快照——回归场景这个「提速」是负优化。

第四刀：容器缓存与 NFS 时间戳，两条环境线。 容器化跑 fm_shell 时，把 Synopsys 用户级缓存挂成宿主机卷可以加速启动，但缓存卷必须按工具版本分目录（如 2025.06 一个卷、老版本另一个卷），跨版本复用会读出不兼容格式的缓存，轻则报警告、重则静默用错配置。NFS 共享卷上，构建机与计算机时钟差几秒，会出现「rtl 文件内容已更新、mtime 却比 svf 旧」的假象，增量判断据此认为输入没变。处置：所有跑链路的机器对时（NTP），构建完成时 touch 一次关键产物强制刷新 mtime，比对前用 md5sum 而非时间戳确认文件确实变了。

第五刀：依赖快照与版本切换。 回归每轮重生成文件清单（find rtl 目录按时间排序落盘），比对前与上一轮 diff，清单没变而 RTL「改了」，直接暴露快照陈旧。工具版本升级（如从老版本切到 2025.06）后第一轮必须全量清缓存重跑，老版本留下的 work 与缓存格式不保证向前兼容，这方面的判据集中见 Formality 版本不匹配速查。

五、防复发与纪律 ​

  • 回归每轮独立 work 目录：命名带时间戳，跑前不继承任何旧目录；保存点只在交互调试用。
  • svf 生日校验进脚本：set_svf 前断言 svf 比综合完成标志新，不满足直接 fail。
  • 缓存卷按版本分目录：容器环境与家目录缓存都按工具版本隔离，升级即换。
  • 全链路对时 + touch 刷新：NFS 环境下构建机、计算机统一 NTP；构建完成 touch 关键产物。
  • 首轮改代码后必做对照实验：改 RTL 后第一轮手动清缓存全量重跑，确认结果会动，再交给回归。
  • 结果一致性监控：回归收尾对比相邻两轮报告，逐字节一致且 RTL 有变更时报警——这正是本篇开头的现场。

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

本篇是 EDA 工具排错速查簇的 FAQ 页，专管 Formality 输入链路上的陈旧产物与缓存复用一条线；工具版本切换导致的缓存格式不兼容在 Formality 版本不匹配速查，上一轮中断写出残缺文件被判陈旧或损坏的处置见 Formality 文件损坏截断速查，清缓存时连带释放 work 目录占盘的方法见 Formality 磁盘写满速查，回归产物整体丢失的分诊见 Formality 回归结果丢失速查。

一句话总结 ​

Formality 改了 RTL 结果不变，先做对照实验——整目录清 work、删旧 svf、按版本隔离缓存后从零全量重跑，结果随 RTL 变化就确认存在陈旧来源，再逐环定位：svf 必须是本次综合产物（比对前校验时间戳）、回归每轮用独立 work 目录不复用保存点、容器缓存卷按工具版本分目录、NFS 全链路对时并用 touch 刷新 mtime、版本升级后首轮全量清缓存；长期靠「svf 生日校验 + 相邻两轮报告一致性监控」两条脚本纪律，让陈旧产物在喂给 fm_shell 之前就被拦下。