2. VC Formal工具链与工程环境

VC Formal 是 Synopsys 形式验证平台中的核心应用，它并不是一个孤立的可执行文件，而是由安装目录、许可证服务、命令行驱动、图形界面、项目工作目录和脚本入口共同组成的一套工程环境。理解这套环境的组织方式，是后续编写断言、运行证明、管理回归和归档结果的前提。本节从安装目录结构入手，逐步展开许可证配置、启动方式、项目目录组织、脚本化入口与结果归档，帮助读者建立一套可复现的工程化使用习惯。

安装目录结构

在典型的 Linux 环境中，VC Formal 随 Synopsys 验证工具套件一起安装，通常位于类似 /tools/synopsys/vcformal/ 的路径下，版本号会体现在目录名中，例如 V-2023.12。安装根目录下一般包含以下关键子目录：

• bin/：存放 vcformal、vcformal_shell 等可执行入口，是命令行启动的核心。
• lib/：工具运行所需的共享库和内部组件，通常不需要用户直接修改。
• include/：提供给用户或集成脚本使用的头文件与接口定义。
• doc/：用户手册、命令参考和发布说明，是查证参数含义的第一手资料。
• examples/：官方示例工程，包含可运行的测试用例和脚本模板，适合作为项目目录组织的参考。
• auxi/ 或 etc/：辅助配置文件和许可证相关模板。

需要特别注意的是，安装目录通常由管理员统一维护，普通用户不应在其中写入项目文件。工程实践中的基本原则是：工具安装目录只读，项目工作目录可写。这样既能避免升级工具时覆盖用户数据，也便于多用户共享同一套安装。

许可证配置

VC Formal 依赖 Synopsys 的许可证服务（License Server）才能启动。许可证配置的核心是让工具知道去哪个服务器、哪个端口获取授权。常见做法是通过环境变量指定：

export SNPSLMD_LICENSE_FILE=27020@lic-server.company.com
export LM_LICENSE_FILE=$SNPSLMD_LICENSE_FILE

其中 27020 是许可证服务端口，lic-server.company.com 是许可证服务器主机名。如果企业使用多个工具套件，也可以把多个许可证路径用冒号分隔。配置完成后，可以用 lmstat 或 Synopsys 自带的 sssverify 检查许可证是否可达。若启动时报出 “Cannot connect to license server” 或 “Invalid license key”，应优先检查网络连通性、端口是否被防火墙拦截，以及许可证文件中是否包含 VC Formal 对应的 feature 名称，例如 VC_Formal 或 VC_Formal_Shell。

命令行与 GUI 启动方式

VC Formal 提供两种主要启动方式：命令行（shell）和图形界面（GUI）。命令行方式适合脚本化、回归和批量运行；GUI 方式适合交互式调试、查看波形和属性状态。

命令行启动的典型形式如下：

vcformal_shell -f run.tcl -l run.log

其中 -f 指定要执行的 Tcl 脚本，-l 指定日志文件。VC Formal 的自动化流程高度依赖 Tcl 命令，例如 read_file、set_top、create_clock、run_formal 等。GUI 启动则可以直接执行 vcformal，然后在界面中加载设计、创建属性并运行证明。对于初学者，GUI 有助于理解属性状态和反例波形；对于工程化流程，命令行才是可重复、可归档的主力方式。

无论哪种方式，启动前都应确认当前工作目录、环境变量和许可证状态。一个常见的做法是先运行 vcformal -version 确认工具版本，再进入正式流程。

项目目录组织

一个清晰的项目目录结构能显著降低回归和归档的复杂度。推荐按“设计、约束、脚本、运行、结果”五个维度组织：

• rtl/：存放待验证的 RTL 源文件，通常以文件列表 rtl.f 管理。
• constraints/：存放时钟、复位、输入假设等 SDC 或 Tcl 约束。
• scripts/：存放主运行脚本、属性文件和环境配置脚本。
• runs/：每次运行的输出目录，按时间戳或标签命名，例如 runs/20240612_baseline/。
• results/：归档最终结果，包括日志、报告、反例波形和覆盖率数据。

这种结构的核心思想是：脚本和输入保持稳定，运行输出按次隔离。每次运行都在 runs/ 下新建目录，避免不同次运行的结果互相覆盖。对于需要对比的场景，可以保留多个运行目录，再用脚本汇总结果。

脚本化运行入口与结果归档

脚本化运行的关键是定义一个稳定的入口脚本，通常命名为 run.tcl 或 run_vcformal.tcl。该脚本负责读取设计、设置顶层、加载约束、读取属性、运行证明并输出报告。一个简化的示例结构如下：

# run.tcl
set TOP top_module
read_file -format verilog -f rtl.f
set_top $TOP
read_sdc constraints/top.sdc
read_file -format tcl -f scripts/properties.tcl
run_formal -mode prove
report_status -file results/status.rpt
report_property -file results/property.rpt

运行结束后，结果归档应至少包含：运行日志 run.log、属性状态报告 status.rpt、反例波形（若有失败属性）、以及本次运行使用的脚本和输入文件列表。归档目录建议按“日期_标签”命名，并在其中保留一份 manifest.txt，记录工具版本、许可证服务器、运行命令和关键参数。这样在后续复盘或回归对比时，可以快速定位到具体环境。

从工程闭环的角度看，安装目录提供工具能力，许可证服务提供启动授权，项目目录组织输入与输出，脚本入口负责执行，结果归档负责留痕。四者缺一不可。实际项目中，建议把许可证检查、版本确认和目录创建也纳入入口脚本的前置步骤，例如在 run.tcl 开头检查 SNPSLMD_LICENSE_FILE 是否设置，或在 shell 包装脚本中先执行 mkdir -p runs/$RUN_TAG。这样即使换机器或换用户，也能快速复现同一套运行环境。

最后，结果归档不只是保存文件，更是保存“可解释性”。一份完整的归档应能让其他人看懂：这次运行用了哪个工具版本、哪个许可证、哪份 RTL、哪组约束、哪条命令，以及每个属性的最终状态。做到这一点，VC Formal 的工程环境才算真正搭建完成。