环境搭建准备：Linux操作系统选择、虚拟机安装、磁盘分区与文件系统规划
说实话，形式化验证工具对环境的要求挺苛刻的。我见过不少新手，工具装到一半卡住了，最后发现是操作系统版本不对。嗯，这一节咱们就把地基打牢。
1. Linux发行版怎么选？
我个人习惯用 CentOS 7.9 或 RHEL 8.6。为什么？
- 形式化验证工具（比如 Cadence JasperGold、Synopsys VC Formal）官方认证的就是这些版本
- 长期支持（LTS），不会突然断更
- 社区资源多，遇到问题好搜
你可能会问：Ubuntu不行吗？我在项目中遇到过用Ubuntu 20.04跑JasperGold，结果license daemon死活起不来。查了两天，最后发现是glibc版本不兼容。所以，别在发行版上玩花活。
我的推荐清单：
- 首选：CentOS 7.9 (2009) —— 最稳，没有之一
- 备选：RHEL 8.6 —— 如果你有红帽订阅
- 不推荐：Ubuntu Desktop、Fedora、Arch Linux
2. 虚拟机安装——别偷懒
我建议用 VMware Workstation Pro 16/17。VirtualBox也行，但我在项目中遇到过VirtualBox的3D加速问题，导致图形界面卡顿。做形式化验证时，你要频繁看波形、调约束，界面卡了真的很崩溃。
安装步骤其实很简单，但有几个坑要注意：
- CPU虚拟化要开：进BIOS把Intel VT-x或AMD-V打开。我曾经帮一个同事排查，他虚拟机死活起不来，就是BIOS里没开这个。
- 内存给够：至少8GB，推荐16GB。形式化验证工具吃内存，你想想看，一个中等规模的模块跑起来，4GB根本不够用。
- 磁盘用厚置备：创建虚拟机磁盘时，选「厚置备延迟置零」。虽然一开始占空间大，但性能比「精简置备」好很多。
小技巧：安装完系统后，记得装VMware Tools。不然你没法自适应分辨率，也没法拖拽文件。我一般用open-vm-tools-desktop包，yum直接装就行。
3. 磁盘分区——别一股脑全给根分区
很多人装Linux时，直接「使用全部磁盘」，结果根分区占了所有空间。这样做，后面有你哭的。
形式化验证工具会产生大量中间文件。比如JasperGold跑一次formal，可能会生成几十GB的日志和数据库。如果根分区满了，工具直接崩溃，你跑了一天的验证就白费了。
我建议这样分区（以500GB磁盘为例）：
| 挂载点 | 大小 | 文件系统 | 说明 |
|---|---|---|---|
| /boot | 1GB | ext4 | 引导分区，不用太大 |
| / | 100GB | ext4 | 系统根分区，够用就行 |
| /home | 100GB | ext4 | 用户数据，脚本、配置文件放这里 |
| /tools | 150GB | ext4 | 安装EDA工具，单独分区方便管理 |
| /data | 剩余全部 | xfs | 验证数据、日志、数据库 |
| swap | 16GB | swap | 交换分区，内存不够时保命用 |
注意：/tools和/data一定要分开。我见过有人把所有工具和项目数据都放根分区，结果根分区满了，系统都进不去。单独分区的好处是，就算/data满了，系统还能正常用，你还能ssh进去清理。
4. 文件系统规划——ext4还是xfs？
嗯，这里有个小讲究。
- ext4：成熟稳定，兼容性好。我建议系统分区（/、/boot、/home）用ext4。
- xfs：大文件性能好，适合存储验证数据。我习惯把/data分区格式化成xfs。形式化验证的数据库文件动辄几十GB，xfs处理大文件比ext4快。
你可能会问：btrfs呢？zfs呢？说实话，我在项目中试过btrfs，结果有一次系统崩溃后文件系统损坏，恢复起来特别麻烦。对于生产环境，别追求新潮，稳字当头。
5. 一张图看懂整体规划
下面这张图，是我自己总结的环境搭建逻辑。你照着这个思路来，基本不会出错。
6. 避坑指南
最后，分享几个我踩过的坑：
- swap分区别太小：我曾经只给了4GB swap，结果跑大规模formal时内存爆了，工具直接OOM被杀。现在我都给16GB。
- 别用LVM：虽然LVM灵活，但形式化验证工具对LVM支持不好。我遇到过JasperGold在LVM上创建数据库时报错，换成普通分区就好了。
- 文件系统别用noatime：有些人为了性能会挂载时加noatime，但形式化验证工具会记录文件访问时间，关了可能导致工具异常。
好了，环境搭建的准备就这些。你按照这个思路来，后面装工具时会省很多事。