第二章：FormalNode工具介绍
各位同学，今天我们来聊聊FormalNode这个工具。说实话，形式验证工具市面上有好几款，但FormalNode是我个人用得最顺手的一个。它不像某些商业工具那么笨重，也不像开源工具那样缺胳膊少腿。嗯，咱们直接进入正题。
2.1 FormalNode工具架构
FormalNode的架构，说白了就是三层结构。我画个图给大家看看，这样更直观。
你看，最上层是用户接口层，说白了就是你怎么跟工具打交道。我个人习惯用Tcl命令行，因为脚本化之后可以批量跑回归。但刚入门的同学可以先从GUI入手，后面我会详细讲。
中间是核心引擎层，这是FormalNode的魂。三个引擎各司其职：属性检查引擎负责验证你的断言对不对，覆盖分析引擎告诉你哪些逻辑被验证到了，形式化简引擎则负责把复杂问题变简单。我在项目中遇到过一个大模块，直接跑属性检查跑了一天没结果，后来用了化简引擎，半小时就出结果了。
底层是数据支撑层，RTL解析器、约束求解器、模型检查器这些基础组件。嗯，这里要注意，约束求解器是形式验证的瓶颈，很多跑不动的情况都是卡在这里。
2.2 FormalNode安装与配置
安装FormalNode其实不复杂，但有几个坑我得提前告诉你。
系统要求
| 项目 | 最低配置 | 推荐配置 |
|---|---|---|
| 操作系统 | CentOS 7 / Ubuntu 18.04 | CentOS 8 / Ubuntu 20.04 |
| CPU | 4核 | 16核以上 |
| 内存 | 8GB | 64GB以上 |
| 磁盘 | 20GB | 100GB SSD |
安装步骤
安装过程其实就三步，我给大家列一下：
- 解压安装包：
tar -xzf FormalNode_2024.1_linux64.tar.gz - 设置环境变量：把bin目录加到PATH里
- 配置license：设置
FN_LICENSE_FILE环境变量
这里有个小技巧。我建议你把环境变量写到.bashrc里，省得每次都要手动设。像这样：
# 在 ~/.bashrc 中添加
export FN_HOME=/tools/FormalNode/2024.1
export PATH=$FN_HOME/bin:$PATH
export FN_LICENSE_FILE=27000@license_serversource ~/.bashrc 或者重新登录终端。我第一次装的时候忘了这步，折腾了半天才发现环境变量没生效。
2.3 FormalNode基本工作流程
FormalNode的工作流程，说白了就是三步走：读设计、设属性、跑验证。你想想看，这不就跟我们做实验一样吗？先准备好样品，再设定测试条件，最后看结果。
具体来说是这样的：
- 读入设计：把RTL代码读进来，FormalNode会自动解析出模块层次和信号连接
- 设定验证属性：用SVA或者内置的断言模板来描述你要验证的行为
- 运行验证：选择验证模式（证明、覆盖、调试），然后启动引擎
我给大家看一个最简单的例子：
# 1. 读入设计
read_verilog -top top_module ./rtl/*.v
# 2. 设定时钟和复位
create_clock clk -period 10
create_reset rst_n -active low
# 3. 添加断言
assert -name "req_ack_handshake" \
-expr "req |=> ##[1:5] ack"
# 4. 运行验证
prove -assertion req_ack_handshake -depth 20这段代码什么意思呢？我们定义了一个握手机制的断言：当req拉高后，在1到5个时钟周期内，ack必须拉高。然后让工具去证明这个属性是否成立。
2.4 FormalNode GUI界面介绍
FormalNode的GUI界面，我刚开始用的时候觉得有点乱，但用顺手了就会发现它设计得挺合理的。主要分这么几个区域：
- 工程管理区：左边栏，显示你的工程文件、模块层次
- 代码浏览区：中间主区域，显示RTL代码
- 结果展示区：下方区域，显示验证结果、波形、反例
- 控制台：底部，显示运行日志和Tcl命令交互
我个人最常用的是结果展示区里的波形查看功能。当形式验证找到一个反例时，它会自动生成一个波形，告诉你从哪个状态开始，经过哪些路径，最终违反了断言。这个功能在调试时特别有用。
Ctrl+L 可以快速定位到当前选中的信号定义。这个快捷键我每天要用几十次。
嗯，说到这里，我想起一个事。有一次我带一个新人做项目，他跑完形式验证看到一堆反例，整个人都懵了。其实反例不是坏事，它恰恰说明你的断言写得好，能抓到bug。关键是要学会看反例波形，一步步追踪问题根源。
好了，关于FormalNode工具的基本介绍就到这里。记住，工具只是工具，真正重要的是你理解形式验证的思想和方法。下一节我们会深入讲断言语言，那才是形式验证的灵魂。
公众号:蓝海资料掘金营，微信deep3321