第二章：Formality环境搭建——软件安装、License配置、环境变量设置、启动与退出
好，咱们正式开始动手了。这一章我带你把Formality跑起来。说实话，环境搭建这事儿看着简单，但坑不少。我见过太多工程师花了一整天装软件，最后卡在License上。咱们一步步来，别急。
2.1 软件安装——选对版本很重要
Formality是Synopsys家的工具。安装包通常叫 Formality_xxxx_common 和 Formality_xxxx_linux。我个人习惯用最新稳定版，别追最新，也别用太老的。
安装步骤其实就三步：
- 解压安装包：把两个tar包解压到同一个目录。
- 运行安装脚本：执行
./installer，按提示走。 - 选择安装路径：我一般放
/tools/synopsys/formality/下，好管理。
关键点：安装时记得选“Full Installation”，别省空间。缺了组件后面跑不起来，更麻烦。
嗯，这里要注意：安装过程中会让你选平台，选 amd64（就是64位Linux）。现在基本没人用32位了。
2.2 License配置——最容易翻车的地方
License配置，说白了就是让工具认你。我刚开始做形式验证时，在这上面折腾了两天。后来发现，其实就是几个环境变量没设对。
你需要准备两样东西：
- License文件：通常是
synopsys.dat或license.dat - SNPSLMD_LICENSE_FILE：指向这个文件的环境变量
配置方式有两种：
| 方式 | 命令示例 | 说明 |
|---|---|---|
| 直接指向文件 | export SNPSLMD_LICENSE_FILE=/tools/licenses/synopsys.dat |
简单直接，适合单机 |
| 指向License Server | export SNPSLMD_LICENSE_FILE=27000@license_server_ip |
适合公司环境，端口号看你们IT怎么配的 |
避坑指南：我曾经遇到过一个问题——License文件里hostname写错了。工具报错说“License check out failed”，我查了半天，最后发现是服务器主机名大小写不匹配。所以，hostname命令先跑一下，确认大小写。
还有一个容易忽略的：LM_LICENSE_FILE 这个变量。有些老版本工具认这个，不认 SNPSLMD_LICENSE_FILE。我建议两个都设上，反正不冲突。
export SNPSLMD_LICENSE_FILE=27000@lic-srv-01
export LM_LICENSE_FILE=27000@lic-srv-012.3 环境变量设置——别漏了这几个
环境变量设置，说白了就是告诉系统“Formality在哪”。我一般写在 .bashrc 或 .cshrc 里，这样每次登录自动加载。
核心变量就这几个：
- SYNOPSYS：指向Formality安装根目录
- PATH：加上
$SYNOPSYS/bin - LD_LIBRARY_PATH：加上
$SYNOPSYS/lib（有些系统需要）
举个例子，我的 .bashrc 里是这样写的：
export SYNOPSYS=/tools/synopsys/formality/F-2011.06-SP2
export PATH=$SYNOPSYS/bin:$PATH
export SNPSLMD_LICENSE_FILE=27000@lic-srv-01
export LM_LICENSE_FILE=27000@lic-srv-01小技巧：设完变量后，跑一下 which fm_shell，看看能不能找到。如果返回路径对了，说明环境变量生效了。如果没找到，检查一下 PATH 里有没有拼错。
你想想看，如果 PATH 没设对，你敲 fm_shell 就会报“command not found”。这种低级错误我犯过一次，后来就学乖了。
2.4 启动与退出Formality——两种模式
Formality有两种启动模式：
- GUI模式：
fm_shell -gui或直接formality & - Tcl模式：
fm_shell -tcl或fm_shell -file script.tcl
我个人习惯：调试时用GUI，跑回归时用Tcl模式。GUI方便看波形和报告，Tcl模式适合批量跑。
启动GUI后，你会看到主界面。嗯，第一次打开可能会有点懵，别怕。左边是导航栏，中间是主工作区，下面是日志窗口。布局跟其他EDA工具差不多。
退出也很简单：
- GUI模式：点右上角关闭，或者菜单栏 File → Exit
- Tcl模式：敲
exit或quit
重要提醒：退出前记得保存会话。GUI模式下，File → Save Session，下次可以直接加载。我经常忘了保存，结果第二天得重新设一遍，烦得很。
2.5 验证环境是否正常——跑个简单的例子
环境搭好了，怎么知道能不能用？跑个最简单的例子试试。
创建一个文件 test.fms，内容如下：
# 加载两个简单的设计
read_verilog -container r -libname WORK {top.v}
read_verilog -container i -libname WORK {top.v}
# 设置顶层
set_top r:/WORK/top
set_top i:/WORK/top
# 跑验证
verify
# 看结果
report_passing
report_failing然后执行：
fm_shell -f test.fms如果输出里有 Verification SUCCEEDED，恭喜你，环境搭好了。如果报错，别慌，看看日志里提示什么。大部分问题都是License或路径没设对。
我的经验：第一次跑验证时，我建议用GUI模式。这样能看到每一步的详细信息，出问题了也容易定位。等熟悉了再用Tcl模式。
好了，环境搭建就这些。下一章咱们开始讲Formality的核心概念——Reference和Implementation。到时候你会明白，为什么形式验证能帮你找到那些仿真发现不了的bug。