精通PSL形式化验证VHDL模块：从理论到实战
为安全关键FPGA应用设计VHDL，仅写测试平台远不够。工程师必须证明模块完全符合规范、无隐藏副作用。形式化验证提供这种数学级保证。
形式化验证通过证明所有可能输入序列均满足设计属性，弥合需求与实现鸿沟。它是医疗器械、航空电子等要求DO-254认证领域的必经之路。
本客座文章由资深形式化验证实践者Michael Finn Jørgensen撰写，分享实战洞见与可落地技巧。示例基于熟悉的AXI FIFO教程如何用就绪/有效握手在块RAM中实现AXI FIFO，演示如何对真实VHDL设计应用PSL。
什么是形式化验证？
形式化验证（FV）是综合前系统性方法，保证设计对所有输入组合正确。不同于依赖人工激励的常规测试平台，FV指定属性，要求所有时钟周期成立。SAT求解器再穷尽证明属性成立——或给出反例精确定位违规周期。
两大核心技术驱动FV：
- 有界模型检查 (BMC) — 从复位起检查有限周期数。
- 归纳证明 — 验证若某状态有效则所有后续状态有效。需完整属性集，但能给出无限周期保证。
BMC仅需少量属性即可运行，常作为第一道防线。归纳证明虽更苛刻，却给出绝对确定性。
为何使用形式化验证？
FV擅长自动探索全输入空间揭露隐蔽缺陷。发现故障时，工具给出精简波形精确指示违规属性的准确周期——远易于调试长仿真波形。
虽FV是强大单元测试工具，不替代手工集成测试。模块规模增长时求解器运行时间可能激增。但投入FV时间能减少总调试工作、加速上市。
在PSL中编写属性
PSL（属性规范语言）是VHDL形式化验证通用语。属性通常存放于单独.psl文件，验证阶段由求解器读取。
三个PSL关键字描述属性：
assert— 保证条件恒真。assume— 陈述输入假设。cover— 检查特定场景是否可达。
PSL文件也可包含普通VHDL声明与进程，便于为复杂断言创建辅助信号。
每个PSL文件以vunit块起始，绑定特定实体：
vunit INSTANCE_NAME(ENTITY_NAME(ARCHITECTURE_NAME)) { }
继以默认时钟声明：
default clock is rising_edge(clk);
属性语法如下：
LABEL : assert always {PRECONDITION} |-> {POSTCONDITION} LABEL : assume always {PRECONDITION} |-> {POSTCONDITION}
用|=> 表达次周期断言：
LABEL : assert always {PRECONDITION} |=> {POSTCONDITION}
条件中可用stable约束信号周期间不变，用{C1; C2}链式表达顺序约束。
安装所需工具链
商业工具（如ModelSim）支持形式化验证，但免费Student Edition缺此功能。幸而Linux（及Windows WSL）有健壮开源栈。下文基于Ubuntu 20.04 LTS，适用任意近期Debian系发行版。
前置依赖
sudo apt update && sudo apt upgrade
安装核心开发库：
sudo apt install build-essential clang bison flex libreadline-dev \ gawk tcl-dev libffi-dev git mercurial graphviz \ xdot pkg-config python python3 libftdi-dev gperf \ libboost-program-options-dev autoconf libgmp-dev \ cmake gnat gtkwave
Yosys与SymbiYosys
git clone https://github.com/YosysHQ/yosys cd yosys make sudo make install cd .. git clone https://github.com/YosysHQ/SymbiYosys cd SymbiYosys sudo make install cd .. git clone https://github.com/SRI-CSL/yices2 cd yices2 autoconf ./configure make sudo make install cd ..
GHDL与Yosys插件
git clone https://github.com/ghdl/ghdl cd ghdl ./configure --prefix=/usr/local make sudo make install cd .. git clone https://github.com/ghdl/ghdl-yosys-plugin cd ghdl-yosys-plugin make sudo make install cd ..
下载示例项目
填写下方表单获取含完整AXI FIFO源码、PSL文件、验证脚本的ZIP包。
实战案例：AXI FIFO形式化验证
下文梳理FIFO关键属性类别并展示PSL编码。
复位处理
f_reset : assume {rst};
省略always关键字，此假设仅作用于复位后首周期。标签约定（f_前缀）便于定位失败。
f_after_reset_valid : assert always {rst} |=> {not out_valid}; f_after_reset_ready : assert always {rst} |=> {in_ready}; f_after_reset_head : assert always {rst} |=> {count = 0};
注意内部信号count可被引用，因vunit声明包含架构名。
FIFO满/空信号
f_empty : assert always {count = 0} |-> {not out_valid}; f_full : assert always {count = ram_depth-1} |-> {not in_ready};
AXI协议合规
f_in_data_stable : assume always {in_valid and not in_ready and not rst} |=> {stable(in_valid) and stable(in_data)}; f_out_data_stable : assert always {out_valid and not out_ready and not rst} |=> {stable(out_valid) and stable(out_data)};
就绪信号稳定性：
f_out_ready_stable : assume always {out_ready and not out_valid and not rst} |=> {stable(out_ready)}; f_in_ready_stable : assume always {in_ready and not in_valid and not rst} |=> {stable(in_ready)};
FIFO顺序性
顺序性保证先写先出。用辅助信号记忆特定数据值进出时刻建模。
signal f_sampled_in_d1 : std_logic := '0'; signal f_sampled_in_d2 : std_logic := '0'; p_sampled : process (clk) begin if rising_edge(clk) then if in_valid then if in_data = f_value_d1 then f_sampled_in_d1 <= '1'; end if; if in_data = f_value_d2 then f_sampled_in_d2 <= '1'; end if; end if; if out_valid then if out_data = f_value_d1 then f_sampled_out_d1 <= '1'; end if; if out_data = f_value_d2 then f_sampled_out_d2 <= '1'; end if; end if; if rst = '1' then f_sampled_in_d1 <= '0'; f_sampled_in_d2 <= '0'; f_sampled_out_d1 <= '0'; f_sampled_out_d2 <= '0'; end if; end if; end process p_sampled;
声明数据值为无约束常量，供求解器任意选择位模式：
signal f_value_d1 : std_logic_vector(ram_width - 1 downto 0); signal f_value_d2 : std_logic_vector(ram_width - 1 downto 0); attribute anyconst : boolean; attribute anyconst of f_value_d1 : signal is true; attribute anyconst of f_value_d2 : signal is true;
最后编码顺序约束：
f_fifo_ordering_in : assume always {f_sampled_in_d2} |-> {f_sampled_in_d1}; f_fifo_ordering_out : assert always {f_sampled_out_d2} |-> {f_sampled_out_d1};
运行形式化验证
为sby工具创建axi_fifo.sby脚本：
[tasks] bmc [options] bmc: mode bmc bmc: depth 10 [engines] smtbmc [script] ghdl --std=08 -gram_width=4 -gram_depth=8 axi_fifo.vhd axi_fifo.psl -e axi_fifo prep -top axi_fifo [files] axi_fifo.psl axi_fifo.vhd
执行验证：
sby --yosys ";yosys -m ghdl" -f axi_fifo.sby
成功运行输出：
[axi_fifo_bmc] DONE (PASS, rc=0)
将depth设大于FIFO深度可确保求解器探索满容量场景。
突变测试
为评估属性集完备性，故意注入微小缺陷——如移除驱动out_valid的逻辑——重跑FV。若求解器报告断言失败，证明属性足以捕获该错误。
失败示例：
Assert failed in axi_fifo: i_axi_fifo.f_out_data_stable
用GTKWave打开生成的trace.vcd定位违规准确周期。
Cover语句
Cover语句用于断言特定场景可达。例：验证FIFO可被填满再清空：
f_full_to_empty : cover { rst = '1'; rst = '0'[*]; rst = '0' and count = ram_depth-1; rst = '0'[*]; rst = '0' and count = 0};
调整sby脚本含cover任务：
[tasks] bmc cover [options] bmc: mode bmc bmc: depth 10 cover: mode cover
成功覆盖输出：
Reached cover statement at i_axi_fifo.f_full_to_empty in step 15.
将count = ram_depth-1改为count = ram_depth将使cover不可达，展示工具对属性精度的敏感度。
后续进阶
VHDL