PSLによるVHDLモジュールの形式的検証マスター

安全クリティカルなFPGAアプリケーション向けVHDL設計において、単にテストベンチを書くだけでは不十分です。エンジニアは、隠れた副作用のない、仕様通りの正確な振る舞いをモジュールがすることを証明する必要があります。形式的検証がその数学的保証を提供します。

形式的検証は、要件と実装のギャップを、すべての可能な入力シーケンスが設計のプロパティを満たすことを証明することで埋めます。医療機器、航空電子システム、DO-254認証が必要なあらゆる分野での認証に不可欠です。

このゲスト投稿では、経験豊富な形式的検証実践者であるMichael Finn Jørgensen氏が、実践的な洞察と実用的なヒントを共有します。以下の例は、おなじみのAXI FIFOチュートリアル「How to make an AXI FIFO in block RAM using the ready/valid handshake」を基に構築され、実際のVHDL設計にPSLを適用する方法を示します。

形式的検証とは？

形式的検証（FV）は、合成前の体系的な手法で、すべての入力組み合わせに対して設計の正しさを保証します。手動で作成した刺激に依存する従来のテストベンチとは異なり、FVはすべてのクロックサイクルで保持されなければならないプロパティを指定します。SATソルバーがこれらのプロパティが満たされることを網羅的に証明し、満たされない場合は反例を特定します。

FVを支える2つの核心技術：

有界モデル検査（BMC） - リセットから始まる有限サイクル数を検査。
帰納法的証明 - ある状態が有効なら、すべての後続状態も有効であることを検証。完全なプロパティセットが必要だが、無限サイクルの保証を提供。

BMCは少数のプロパティでも実行可能なため、しばしば第一防衛線となります。帰納法はより要求が厳しいですが、絶対的な確実性をもたらします。

なぜ形式的検証を使うのか？

FVは入力空間全体を自動的に探索するため、捉えにくいバグの発見に優れます。欠陥発見時、ツールはプロパティが違反した正確なサイクルを特定する簡潔な波形を生成します。これは長いシミュレーショントレースのデバッグよりはるかに容易です。

FVは強力なユニットテストツールですが、手作りの統合テストを置き換えるものではありません。モジュールサイズが大きくなると、ソルバーの実行時間が問題になることがあります。それでも、FVに時間を投資することは、全体的なデバッグ作業を削減し、市場投入までの時間を短縮します。

PSLでのプロパティ記述

PSL（Property Specification Language）は、VHDLにおける形式的検証の共通言語です。プロパティは通常、検証フェーズでソルバーが読み取る別の.pslファイルに格納されます。

プロパティを記述する3つの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};

vunit宣言にアーキテクチャ名が含まれるため、countなどの内部信号を参照可能です。

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

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順序保証

順序保証は、早い書き込みが遅い書き込みより先に出力されることを意味します。特定のデータ値が入力または出力されたタイミングを記憶する補助信号でモデル化します。

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

生成されたtrace.vcdをGTKWaveで開き、プロパティ違反の正確なサイクルを特定します。

カバーステートメント

カバーステートメントは、特定シナリオが到達可能かをアサートするのに有用です。例えば、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スクリプトを調整してカバータスクを含める：

[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に変更するとカバーが到達不能になり、ツールのプロパティ精度への感度を示します。

次のステップ

VUnit 101：自動化VHDL検証の実践ガイド Xilinx Vivadoをマスターする: 統合ロジック・アナライザ(ILA)とバーチャル入出力(VIO)によるデバッグ

VHDL