使用 PSL 在 VHDL 中进行形式化验证

在为安全关键型 FPGA 应用设计 VHDL 时，尽最大努力编写测试平台是不够的。您必须出示该模块按预期工作且没有不良副作用的证据。

形式验证技术可以帮助您将需求映射到测试，证明您的 VHDL 模块符合规范。它是验证医疗保健应用或获得 DO-254 机载 FPGA 解决方案认证的工具。

为了揭开形式验证的神秘面纱，VHDLwhiz 在 Michael Finn Jørgensen 的帮助下撰写了这篇客座文章。 Michael 在该主题方面拥有丰富的经验，并在他的 GitHub 页面上分享了许多技巧。

本文可下载示例中的待测设备来自现有教程：
如何使用就绪/有效握手在块 RAM 中制作 AXI FIFO

我会让 Michael 从这里接手，并在这篇博文的其余部分向你解释形式验证。

什么是形式验证？

形式验证 (FV) 的目的是确保您的模块按预期工作！

FV 是您在合成模块之前作为开发过程的一部分所做的事情。它有时被称为“属性检查”，我认为这是一个更好的描述。

在 FV 中，您指定 properties 您的模块必须具有，然后该工具（称为“可满足性求解器”）将证明 您的模块满足所有可能的输入序列的属性 .

换句话说，该工具将查找从 有效的 状态（所有属性都满足）到 invalid 状态（其中一个或多个属性被违反）。如果没有这样的转换，即无法转换到无效状态，则证明属性始终满足。

FV 的挑战是用工具可以理解的语言表达模块的属性。

形式验证是手动编写测试平台的替代方法。形式验证和手动测试台的目的都是为了消除设计中的错误，但形式验证通过检查属性并自动生成许多不同的测试台来做到这一点。

这些工具使用两种不同的方法：

• 有界模型检查 (BMC) . 从复位开始并检查固定数量的时钟周期。
• 归纳证明 .从任意有效状态开始，并验证任何后续状态也有效。

归纳证明更难满足，因为它需要 all 需要说明的属性，而 BMC 可以只用几个属性运行，并且仍然给出有用的结果。

为什么要使用形式验证？

形式化验证非常擅长捕捉难以发现的错误！这是因为形式验证会自动搜索可能输入的整个空间。

这与需要手工制作刺激的传统测试平台编写形成鲜明对比。使用手动编写的测试平台探索整个状态空间几乎是不可能的。

此外，当形式验证确实发现了错误时，它会生成一个非常短的波形来显示错误，并且比基于手动编写的测试平台运行模拟要快得多。这种短波形比通常由仿真产生的非常长的波形更容易调试。

但是，形式验证并不能替代测试台编写。根据我的经验，形式验证非常适合单元测试，而使用手工制作的测试平台进行集成测试会更好。这是因为形式验证的运行时间随着模块的大小呈指数增长。

确实存在与形式验证相关的学习曲线，但值得花时间，我希望这篇博文能帮助您克服这条学习曲线。您将更快地完成设计，并且错误更少！

如何在 PSL 中编写属性

在进行形式验证时，您必须使用属性规范语言 (PSL) 来表达模块的属性。这些属性通常位于以 .psl 结尾的单独文件中 ，并且这个文件只在形式验证时使用。

在本节中，我将笼统地描述 PSL 语言的主要特征，在后面的部分中，我将通过一个具体的例子来告诉你。

PSL中有3个语句：

• assert
• assume
• cover

您可能已经熟悉关键字 assert 在编写测试平台时。 PSL 中也使用了相同的关键字，但语法略有不同。 assert 关键字用于描述此模块承诺始终满足的属性。特别是 assert 关键字应用于模块的输出，或者也可能应用于内部状态。

assume 关键字用于描述此模块对输入的任何要求。换句话说，assume 关键字应用于模块的输入。

cover 关键字用于描述必须以某种方式实现的属性。

您也可以在 PSL 文件中编写常规 VHDL 代码，包括信号声明和处理（同步和组合）。

PSL 文件的第一行应该是

vunit INSTANCE_NAME(ENTITY_NAME(ARCHITECTURE_NAME)) {

这里ENTITY_NAME 和 ARCHITECTURE_NAME 请参阅您正在验证的模块。 INSTANCE_NAME 可以是你喜欢的任何东西。该文件应以右大括号结尾：} .

.psl 中的下一行 文件应该是：

default clock is rising_edge(clk);

这样可以避免在每个属性语句中繁琐地引用时钟信号。

assert 的语法 和 assume 陈述是：

LABEL : assert always {PRECONDITION} |-> {POSTCONDITION}
LABEL : assume always {PRECONDITION} |-> {POSTCONDITION}

该语句内容如下： 如果 PRECONDITION 保持（在任何时钟周期）然后 POSTCONDITION 必须满足相同 时钟周期。

还有一种常用的形式：

LABEL : assert always {PRECONDITION} |=> {POSTCONDITION}

该语句内容如下： 如果 PRECONDITION 保持（在任何时钟周期）然后 POSTCONDITION 必须满足下一个 时钟周期。

这两种形式都被广泛使用。

PRE- 内 和 POST-CONDITIONS ，可以使用关键字stable . this关键字的意思是：this中的值 时钟周期与previous中的值相同 时钟周期。

PRE- 内 和 POST-CONDITIONS ，你也可以使用序列，写成如下：

{CONDITION_1 ; CONDITION_2}

这意味着 CONDITION_1 必须满足this 时钟周期和那个 CONDITION_2 必须满足下一个 时钟周期。

封面语句的语法如下：

LABEL : cover {CONDITION}

我们将在本博客后面的示例中看到所有这些语句的大量示例。

安装所需工具

包括 ModelSim 在内的领先工具供应商都支持形式验证。不幸的是，ModelSim 学生版不支持形式验证。确实，您收到以下错误：

所以使用 ModelSim 进行形式验证需要付费许可。

相反，有一些开源（免费）工具可以让您进行形式验证。在本节中，我将指导您完成这些工具的安装过程。

本指南假定您在 Linux 平台上运行。如果您使用的是 Windows 平台，我建议您使用适用于 Linux 的 Windows 子系统 (WSL)。以下指南使用 Ubuntu 20.04 LTS 进行验证。

先决条件

首先，我们必须更新系统以获得最新的补丁：

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 等人。

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 等

GHDL有预打包的二进制文件，但我建议下载最新的源文件并编译如下：

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 ..

下载示例项目

本文的下一部分将指导您完成对现有 VHDL 项目的形式验证。您可以通过在下面的表格中输入您的电子邮件地址来下载完整的代码。

形式验证的工作示例

以下部分将介绍如何正式验证之前在本博客上写的 axi_fifo 模块。

要开始形式化验证，我们需要问自己，FIFO 有哪些属性？我已经确定了四类属性：

• 复位处理：模块在复位后以明确定义的状态唤醒。
• FIFO 满和空信号：验证 FIFO 是否正确指示满和空情况。
• AXI 协议：模块满足 AXI 有效/就绪握手的要求。
• FIFO 排序：FIFO 不会丢弃/复制/重新排序通过它的元素。

我将在下面讨论这些属性。

重置处理

首先，我们声明模块期望在一个时钟周期内断言复位：

f_reset : assume {rst};

注意这里没有关键字 always .没有 always 关键字，该语句仅适用于第一个时钟周期。

给每个正式声明一个标签是习惯的（并且非常有用）。在运行形式验证时，该工具将在报告任何故障时参考这些标签。我使用在所有此类标签前面加上 f_ 的约定 .

然后我们声明重置后FIFO必须为空：

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};

请注意，可以引用 internal 模块中的信号，而不仅仅是端口。这里我们引用count ，这是当前的填充水平，即当前在 FIFO 中的元素数量。这是可能的，因为我们在 PSL 文件的第一行引用了架构名称。

我们也可以在 PSL 文件中有一个单独的进程来计算进出 FIFO 的元素数量。虽然这是首选，但我将使用内部计数信号来保持这篇博文的简短和重点。

FIFO 满和空信号

AXI FIFO 信号满和空的方式是使用 out_valid 和 in_ready 信号。 out_valid 只要 FIFO 不为空，信号就会被置位，并且 in_ready 只要 FIFO 未满，信号就会被置位。让我们检查一下这些属性：

f_empty : assert always {count = 0} |-> {not out_valid};
f_full : assert always {count = ram_depth-1} |-> {not in_ready};

AXI 协议

有效/就绪 AXI 握手表明数据传输仅在两个 valid 时发生 和 ready 被同时断言。使用此协议时的一个典型错误是断言有效（和随附的数据）而不是检查就绪。换句话说，如果 valid 被断言并且 ready 不是，那么 valid 应在下一个时钟周期保持有效，并且数据应保持不变。这适用于进入 FIFO 的数据和从 FIFO 出来的数据。对于进入 FIFO 的数据，我们使用 assume 关键字，对于来自 FIFO 的数据，我们使用 assert 关键字。

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)};

注意这里使用 stable 关键字与 |=> 组合 操作员。这些语句引用了两个连续的时钟周期。在第一个时钟周期，它检查是否 valid 被断言并且 ready 没有断言。然后在下一个（第二个）时钟周期（由 |=> 指示 运算符），valid的值 和 data 应该与前一个（即第一个）时钟周期相同。

其次，对于 AXI 协议，我们要求 ready 信号稳定。这意味着如果 FIFO 可以接受数据（ready 被断言）但没有数据输入（valid 未断言），然后在下一个时钟周期 ready 应该保持断言。

f_out_ready_stable : assume always
   {out_ready and not out_valid and not rst} |=>
   {stable(out_ready)};

f_in_ready_stable : assert always
   {in_ready and not in_valid and not rst} |=>
   {stable(in_ready)};

先进先出排序

FIFO 的另一个重要特性是数据不会被复制/删除/交换。在 PSL 中表达这个属性是相当复杂的，这是这个形式验证中最难的部分。让我们一步一步仔细地浏览这个属性。

一般来说，如果任何数据 D1 先于其他数据 D2 进入 FIFO，那么在输出端，相同的数据 D1 必须在 D2 之前离开 FIFO。

为了在 PSL 中表达这一点，我们需要一些辅助信号：f_sampled_in_d1 , f_sampled_in_d2 , f_sampled_out_d1 , 和 f_sampled_out_d2 .这些信号在复位时被清除，并在 D1 或 D2 进入或离开 FIFO 时被置位。一旦置位，这些信号将保持置位。

所以我们用两部分来表达 FIFO 排序属性：首先是一个假设 即一旦 D2 进入了 FIFO，那么 D1 之前已经进入了：

f_fifo_ordering_in : assume always
   {f_sampled_in_d2} |->
   {f_sampled_in_d1};

其次是一个断言 即一旦 D2 离开了 FIFO，那么 D1 之前已经离开了：

f_fifo_ordering_out : assert always
   {f_sampled_out_d2} |->
   {f_sampled_out_d1};

我们仍然需要声明和填充上面提到的采样信号。我们对输入采样信号进行如下处理：

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;

这里我们引用了另外两个信号，f_value_d1 和 f_value_d2 .它们包含数据值 D1 和 D2。这些信号可以包含任何任意 值，并且有一种特殊的方式可以向形式验证工具表明这一点：

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;

anyconst 属性被形式验证工具识别。表示该工具可以在其位置插入任意常数值。

综上所述，我们已经指定了FIFO的属性。

运行形式验证

在我们真正运行形式验证工具之前，我们需要编写一个小脚本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

[tasks] 部分 声明我们要进行有界模型检查。 [options] 部分 指定 BMC 应运行 10 个时钟周期。默认值为 20。[engines] 部分 选择使用几个不同求解器中的哪一个。根据您的特定设计，不同可能的引擎的执行速度可能会有所不同。现在，保持这个值不变。

[script] 部分是有趣的部分。在这里，我们指定 VHDL 标准 (2008)、泛型值、要处理的文件以及顶级实体的名称。最后，[files] 部分再次包含文件名。

准备好此脚本后，我们可以使用以下命令运行实际的形式验证：

sby --yosys ";yosys -m ghdl"; -f axi_fifo.sby

运行形式化验证工具以不客气的语句结束：

[axi_fifo_bmc] DONE (PASS, rc=0)

这仅仅意味着我们指定的所有属性都满足最多 10 个时钟周期的所有任意输入。增加深度会导致求解器的执行时间更长。但是，请注意深度大于 FIFO 的深度，这意味着 BMC 将遇到某些输入序列的 FIFO 已满情况。如果我们只选择 5 个时钟周期，那么形式验证将永远不会遇到 FIFO 已满，也不会捕获任何与此相关的错误。

可以证明 all 的属性都满足 使用感应证明的时钟周期。但是，这需要更多的工作来编写属性。挑战在于，到目前为止，我们刚刚写了 一些 特性。但是对于归纳，我们需要指定 all 属性（或至少足够多）。这将非常耗时，因此，我将讨论另一种提高我们信心的策略。

变异

所以现在我们已经描述了 axi_fifo 的一些属性 模块必须满足，我们的工具会快速确认这些属性，即证明它们是满足的。但是我们可能还是会有这种不安的感觉：我们确定没有bug吗？我们真的表达了axi_fifo的所有属性吗？ 模块？

为了帮助回答这些问题并对指定属性的完整性更有信心，我们可以应用一种称为 mutation 的技术 :我们特意在实现上做一个小改动，即刻意引入一个bug，然后看看形式验证能不能捕捉到这个bug！

其中一项更改可能是删除一些控制 out_valid 的逻辑 信号。例如，我们可以注释掉这三行：

if count = 1 and read_while_write_p1 = '1' then
  out_valid_i <= '0';
end if;

当我们现在运行形式验证时，我们会收到一条失败消息

Assert failed in axi_fifo: i_axi_fifo.f_out_data_stable
Writing trace to VCD file: engine_0/trace.vcd

使用 GTKwave 工具可以查看附带的波形，如下所示：

在这里我们看到在 40 ns，out_valid 信号应该变为零，但事实并非如此。失败的断言是在 50 ns，其中 out_valid 仍然很高，但 out_data 信号变化，表示重复数据。由于 out_ready 重复数据实际上并未在此特定跟踪中传输 低到 40 ns，但形式验证仍然检测到错误。

封面声明

最后让我们转向形式验证工具的另一种应用：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};

真是满满当当啊！注意 {} 中的分号 .为了便于阅读，我将每个部分放在单独的一行上。该封面声明如下：寻找满足的输入序列：

• 在一个时钟周期内置位复位。
• 然后可以通过任意数量的时钟周期（未断言复位）。
• 一个时钟周期，其中未置位复位且 FIFO 已满。
• 然后可以通过任意数量的时钟周期（未断言复位）。
• 一个时钟周期，其中未置位复位且 FIFO 为空。

所以语法 [*] 表示重复（零次或多次）前面的条件。在第 3 行，我们可以删除条件 rst = '0' 在 [*] 前面 .结果将是相同的。原因是正式验证者会尝试找到最短的 满足覆盖语句的序列，并且在填充 FIFO 时断言重置只会延迟该过程。但是，在第 5 行清空 FIFO 时，必须不断言复位。

现在要运行形式验证器，我们必须对脚本 axi_fifo.sby 进行小修改 .将顶部部分替换为以下内容：

[tasks]
bmc
cover

[options]
bmc: mode bmc
bmc: depth 10
cover: mode cover

现在求解器将运行 BMC，然后运行覆盖分析。在输出中你会看到这两行：

Reached cover statement at i_axi_fifo.f_full_to_empty in step 15.
Writing trace to VCD file: engine_0/trace5.vcd

这意味着cover语句确实可以满足15个时钟周期的序列，并且求解器已经为这个cover语句生成了专门的波形：

在这里，我们看到 80 ns 的 FIFO 已满，in_ready 被取消断言。在 150 ns 时，FIFO 为空并且 out_valid 被取消断言。注意在 30 ns 到 80 ns 期间，out_ready 保持在低位。这对于确保 FIFO 被填满是必要的。

如果我们替换条件 count = ram_depth-1 使用 count = ram_depth ，不能满足封面声明。然后工具会报错。

Unreached cover statement at i_axi_fifo.f_full_to_empty.

因此错误消息包含失败的封面语句的标签。这就是标签如此有用的原因之一！我们将上述错误解释为 FIFO 永远无法容纳 ram_depth 元素的数量。这与原始 AXI FIFO 博客文章中所述完全相同。

从这里去哪里

• PSL 语言入门
• 形式验证简介
• 形式验证入门的一系列小视频
• 与形式验证相关的博客
• 形式验证中更高级主题的系列文章
• 使用形式验证的小示例集合