4. 工程环境搭建

Formality 的等价验证不是“打开工具点一下”就能完成的工作。一个可复现、可交接、可回归的验证环境，决定了后续几十个模块的验证效率。本节从安装、License、目录、脚本模板到版本控制，给出一套可直接落地的工程化搭建方法。

一、安装与版本选择

Formality 通常随 Synopsys Fusion Compiler / Design Compiler 安装包一起分发，安装介质为 .spf 或 .tar.gz 形式。推荐使用 Synopsys Installer 统一安装，而不是手工解包，因为 Installer 会生成 synopsys_installer 的元数据，便于后续打补丁和版本切换。

# 以 Installer 方式安装到统一工具根目录
./Installer -i ./fm_2023.03.spf -install_as_default false \
            -dir /tools/synopsys/formality/R-2023.03-SP2

# 安装完成后设置环境变量（写入项目 env.sh）
export SYNOPSYS=/tools/synopsys
export FM_HOME=$SYNOPSYS/formality/R-2023.03-SP2
export PATH=$FM_HOME/bin:$PATH
export LM_LICENSE_FILE=27020@lic-srv.corp.local

版本选择上，Formality 的版本必须与综合工具（DC/FC）保持兼容。经验做法是：Formality 版本不低于综合工具版本，且尽量使用同一发布周期（如 R-2023.03 对 R-2023.03）。若综合使用 FC R-2023.03，而 Formality 使用 R-2022.06，可能在 SVF 解析、UPF 处理上出现不兼容告警。建议在项目 env.sh 中固定版本号，禁止使用 latest 软链接，避免不同工程师拿到不同版本导致结果不可复现。

二、License 管理

Formality 的核心 License 特性为 Formality（基础等价验证）与 Formality-Adv（含 UPF、增量验证等高级特性）。License 通过 LM_LICENSE_FILE 或 SNPSLMD_LICENSE_FILE 指向 license server，端口格式为 port@host。

# 检查 license 可用性
lmutil lmstat -c 27020@lic-srv.corp.local -f Formality
lmutil lmstat -c 27020@lic-srv.corp.local -f Formality-Adv

# 在 fm 脚本中指定 license 队列（避免抢占其他项目 license）
set_app_var license_queue "fm_project_a"

工程上建议为 Formality 单独申请 license 队列，并在脚本中通过 set_app_var license_queue 绑定，防止与其他项目争抢。若出现 License request failed，优先检查三件事：server 是否可达（ping + telnet port）、feature 是否过期（lmstat -a）、以及是否被 license_queue 限制。对于批量回归，建议在调度脚本中加 license 预检，避免任务排队到一半才失败。

三、工作目录组织

Formality 工程目录应遵循“输入、脚本、运行、报告”四分离原则，避免把 RTL、网表、脚本、日志混在同一层。推荐结构如下：

fm_project/
├── env.sh                 # 工具版本、license、路径
├── scripts/
│   ├── fm_setup.tcl       # 通用变量与库设置
│   ├── run_fm.tcl         # 主流程脚本
│   └── fm_verify.tcl      # 结果检查与退出码
├── inputs/
│   ├── rtl/               # 参考设计（RTL）
│   ├── netlist/           # 实现设计（网表）
│   ├── svf/               # 综合生成的 SVF
│   └── upf/               # 低功耗约束
├── work/                  # 运行目录（每次 run 独立子目录）
│   └── run_20240612_01/
├── reports/               # 汇总报告
└── logs/                  # 运行日志

每次运行在 work/ 下创建带时间戳的子目录，所有中间文件（fm_shell.log、formality_svf、match.rpt）都落在该目录内。这样既方便并行回归，也方便问题复现——只要保留该 run 目录，就能完整回放。

四、脚本模板

一个可复用的 Formality 脚本模板应包含：读入参考设计与实现设计、设置 SVF、执行匹配与验证、输出报告并返回退出码。以下为示例模板（参数为教学示例，非实测结果）：

# run_fm.tcl
set_app_var search_path ". ./inputs/rtl ./inputs/netlist"
set_app_var link_library "* saed32rvt_ss0p75v125c.db"
set_app_var svf_file "./inputs/svf/top.svf"

read_verilog -container r -libname WORK ./inputs/rtl/top.v
read_verilog -container i -libname WORK ./inputs/netlist/top.v
set_top top

# 加载 SVF，处理综合优化引入的寄存器重命名
set_svf $svf_file

# 匹配与验证
match
verify

# 输出报告
report_unmatched_points > ./reports/unmatched.rpt
report_failing_points  > ./reports/failing.rpt
report_passing_points  > ./reports/passing.rpt

# 退出码：0 通过，1 失败
if {[get_app_var verification_status] == "SUCCEEDED"} {
    exit 0
} else {
    exit 1
}

模板中 set_svf 是关键：它告诉 Formality 综合阶段做了哪些优化（如寄存器复制、时钟门控插入、边界优化），否则会出现大量“假失败”。verification_status 用于驱动 CI 退出码，是自动化回归的基础。

五、版本控制集成

Formality 工程应纳入 Git 管理，但需明确哪些文件入库、哪些忽略。建议：

• 入库：env.sh、scripts/*.tcl、inputs/svf/、inputs/upf/、Makefile、.gitignore。
• 忽略：work/、logs/、reports/、*.log、*.svf.bak、formality_svf/。
• 大文件：RTL 与网表若体积大，可用 Git LFS 或外部存储，但需在 README 中记录版本与校验和。

CI 集成时，建议用 Makefile 封装入口，例如 make fm 调用 fm_shell -f scripts/run_fm.tcl，并根据退出码判定流水线通过与否。每次提交触发一次 Formality 回归，可及早发现综合脚本或 RTL 改动引入的等价性问题。