PSL を使用した VHDL でのフォーマル検証

セーフティ クリティカルな FPGA アプリケーション用に VHDL を設計する場合、ベストエフォートでテストベンチを作成するだけでは十分ではありません。モジュールが意図したとおりに動作し、望ましくない副作用がないという証拠を提示する必要があります。

正式な検証手法は、要件をテストにマッピングして、VHDL モジュールが仕様に準拠していることを証明するのに役立ちます。これは、ヘルスケア アプリケーションを検証したり、空中 FPGA ソリューションの DO-254 認証を取得したりするためのツールです。

正式な検証を分かりやすく説明するために、VHDLwhiz は Michael Finn Jørgensen の助けを借りてこのゲスト投稿を書きました。 Michael はこのトピックで豊富な経験を持ち、彼の GitHub ページで多くのヒントを共有しています。

この記事のダウンロード可能なサンプルのテスト対象デバイスは、既存のチュートリアルからのものです:
レディ/有効ハンドシェイクを使用してブロック RAM に AXI FIFO を作成する方法

ここからは Michael に任せて、このブログ投稿の残りの部分で正式な検証について説明します。

正式な検証とは?

フォーマル検証 (FV) の目的は、モジュールが意図したとおりに動作することを確認することです!

FV は、モジュールを合成する前に、開発プロセスの一部として行うものです。 「プロパティ チェック」と呼ばれることもありますが、その方が適切な説明だと思います。

FV で プロパティ を指定します モジュールが持つ必要があり、ツール (「充足可能性ソルバー」と呼ばれる) が証明します。 モジュールが考えられるすべての入力シーケンスのプロパティを満たすこと .

つまり、ツールは 有効な からの遷移を探します。 状態 (すべてのプロパティが満たされた状態) を 無効 にします 状態 (1 つ以上のプロパティが違反されている場所)。そのような遷移がない場合、つまり、無効な状態に遷移する方法がない場合、プロパティは常に満たされていることが証明されています。

FV での課題は、ツールが理解できる言語でモジュールのプロパティを表現することです。

フォーマル検証は、手動で記述されたテストベンチに代わるものです。フォーマル検証と手動テストベンチの両方の目的は、設計からバグを排除することですが、フォーマル検証では、プロパティを調べてさまざまなテストベンチを自動的に生成することでこれを行います。

ツールは 2 つの異なる方法を使用します:

• 境界モデル チェック (BMC) . リセットから開始し、一定数のクロック サイクルを調べます。
• 誘導証明 .任意の有効な状態から開始し、後続の状態も有効であることを確認します。

誘導証明はすべてが必要なため、満たすのがより困難です。 一方、BMC はいくつかのプロパティで実行でき、有用な結果が得られます。

正式な検証を使用する理由

フォーマル検証は、見つけにくいバグを見つけるのに非常に優れています。これは、正式な検証が可能な入力の全空間を自動的に検索するためです。

これは、刺激を手作業で作成する必要がある従来のテストベンチ作成とは対照的です。手動で作成されたテストベンチを使用して状態空間全体を調査することは事実上不可能です。

さらに、フォーマル検証でバグが検出されると、バグを示す非常に短い波形が生成され、手動で記述されたテストベンチに基づいてシミュレーションを実行する場合よりもはるかに高速に実行されます。この短い波形は、通常シミュレーションで発生する非常に長い波形よりもデバッグがはるかに簡単です。

ただし、正式な検証はテストベンチの作成に代わるものではありません。私の経験では、フォーマル検証は単体テストに適していますが、手作りのテストベンチを使用して統合テストを行う方が適しています。これは、フォーマル検証の実行時間がモジュールのサイズに応じて指数関数的に増加するためです。

正式な検証に関連する学習曲線は確かにありますが、時間をかける価値は十分にあります。このブログ投稿が、この学習曲線を乗り越えるのに役立つことを願っています.設計が早く完成し、バグが少なくなります!

PSL でプロパティを記述する方法

正式な検証を行う場合、Property Specification Language (PSL) を使用してモジュールのプロパティを表現する必要があります。プロパティは通常、末尾が 07 の別のファイルにあります。 、このファイルは正式な検証中にのみ使用されます。

このセクションでは、PSL 言語の主な機能を一般的な用語で説明し、後のセクションで具体的な例を紹介します。

PSL には 3 つのステートメントがあります:

• 17
• 29
• 30

キーワード 42 はすでにご存知かもしれません テストベンチを書くとき。これと同じキーワードが PSL でも使用されますが、構文が少し異なります。 57 キーワードは、このモジュールが常に満たされると約束するプロパティを記述するために使用されます。特に、67 キーワードは、モジュールからの出力に適用されるか、内部状態にも適用される可能性があります。

79 キーワードは、このモジュールが入力に課す要件を記述するために使用されます。つまり、81 キーワードがモジュールへの入力に適用されます。

90 キーワードは、何らかの方法で達成できなければならないプロパティを記述するために使用されます。

PSL ファイルには、シグナル宣言とプロセス (同期と組み合わせの両方) を含む通常の VHDL コードも記述できます。

PSL ファイルの最初の行は

vunit INSTANCE_NAME(ENTITY_NAME(ARCHITECTURE_NAME)) {

こちら 105 と 118 検証しているモジュールを参照してください。 122 あなたが好きなものにすることができます。ファイルは閉じ括弧で終わる必要があります:136 .

149 の次の行 ファイルは次のとおりです:

default clock is rising_edge(clk);

これにより、各プロパティ ステートメントでクロック信号を参照する手間が省けます。

158 の構文 と 166 ステートメントは:

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

このステートメントは次のようになります。 184 を (任意のクロック サイクルで) 保持します。 同じで満足する必要があります クロック サイクル。

別の一般的に使用される形式があります:

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

このステートメントは次のようになります:194 204 を (任意のクロック サイクルで) 保持します。 次で満足する必要があります クロック サイクル。

どちらの形式も広く使用されています。

215 内 と 222 、キーワード 231 を使用できます .このキーワードの意味:this の値 クロック サイクルは 前の の値と同じです クロック サイクル。

242 内 と 258 、次のように記述することで、シーケンスも使用できます:

{CONDITION_1 ; CONDITION_2}

つまり、260 これで満足しなければなりません クロックサイクルとその 270 次で満足する必要があります クロック サイクル。

cover ステートメントの構文は次のとおりです:

LABEL : cover {CONDITION}

このブログの後半の実際の例で、これらすべてのステートメントの例をたくさん見ることができます。

必要なツールのインストール

フォーマル検証は、ModelSim を含む主要なツール ベンダーによってサポートされています。残念ながら、ModelSim の Student Edition は正式な検証をサポートしていません。実際、次のエラーが表示されます:

そのため、正式な検証に ModelSim を使用するには、有料ライセンスが必要です。

代わりに、正式な検証を行うためのオープンソース (無料) ツールがあります。このセクションでは、これらのツールのインストール プロセスについて説明します。

このガイドは、Linux プラットフォームで実行していることを前提としています。 Windows プラットフォームを使用している場合は、Windows Subsystem for Linux (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

ヨシスら

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 にはどのようなプロパティがあるのか​​を自問する必要があります。プロパティの 4 つのカテゴリを特定しました:

• リセット処理:モジュールがリセット後に明確に定義された状態でウェイクアップすること。
• FIFO フルおよびエンプティ シグナリング:これは、FIFO がフルおよびエンプティの状態を正しく示していることを確認します。
• AXI プロトコル:モジュールが AXI valid/ready ハンドシェイクの要件を満たしていること。
• FIFO の順序付け:FIFO が通過する要素をドロップ/複製/再順序付けしないこと。

以下で、これらの各プロパティについて説明します。

リセット処理

まず、モジュールがリセットが 1 クロック サイクルの間アサートされることを期待していることを宣言します。

f_reset : assume {rst};

ここでキーワード 283 がないことに注意してください . 294 なし キーワード、ステートメントは最初のクロック サイクルの間だけ保持されます。

各公式ステートメントにラベルを付けるのが慣例です (そして非常に便利です)。正式な検証を実行すると、ツールはエラーを報告するときにこれらのラベルを参照します。そのようなラベルの前に 305 を付けるという規則を使用しています .

次に、リセット後に 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 を参照できることに注意してください。 ポートだけでなく、モジュール内の信号。ここでは 313 を参照します これは、現在の充填レベル、つまり現在 FIFO にある要素の数です。これは、PSL ファイルの最初の行でアーキテクチャ名を参照しているため可能です。

あるいは、FIFO に出入りする要素の数をカウントする PSL ファイルに別のプロセスを含めることもできます。それが望ましいのですが、このブログ投稿を短く簡潔にするために、内部カウント シグナルを使用します。

FIFO のフルおよび空のシグナリング

AXI FIFO がフルとエンプティを通知する方法は、328 を使用することです。 と 331 信号。 349 FIFO が空でない場合は常に信号がアサートされ、356 FIFO がフルでない場合は常に信号がアサートされます。これらのプロパティを確認しましょう:

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

AXI プロトコル

有効/準備完了の AXI ハンドシェイクは、データ転送が両方の 363 の場合にのみ発生することを示しています。 と 373 同時にアサートされます。このプロトコルを使用する際の典型的なエラーの 1 つは、有効 (および付随するデータ) をアサートし、準備完了をチェックしないことです。つまり、387 の場合 アサートされ、393 そうでない場合、403 次のクロック サイクルでアサートされたままになり、データは変更されないままになります。これは、FIFO に入るデータと FIFO から出てくるデータの両方に当てはまります。 FIFO に入るデータには、416 を使用します。 キーワードを使用し、FIFO からのデータには 428 を使用します キーワード。

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

ここで 432 の使用に注意してください 445 と組み合わせたキーワード オペレーター。これらのステートメントは、2 つの連続するクロック サイクルを参照します。最初のクロック サイクルで、452 かどうかをチェックします。 アサートされ、460 主張されていません。次に、次の (2 番目の) クロック サイクル (475 で示されます) operator)、489 の値 そして 499 前の (つまり、最初の) クロック サイクルと同じである必要があります。

次に、AXI プロトコルの場合、504 が必要です。 信号が安定しています。これが意味することは、FIFO がデータ (511) を受け入れることができるかどうかです。 がアサートされます) が、データが入力されていません (524 アサートされていない)、次のクロック サイクル 531 アサートされたままにする必要があります。

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 の順序付け

FIFO のもう 1 つの重要な特性は、データが複製/削除/交換されないことです。このプロパティを PSL で表現するのは非常に複雑であり、これがこの正式な検証の最も難しい部分です。このプロパティを段階的に注意深く見ていきましょう。

一般に、データ D1 が他のデータ D2 の前に FIFO に入る場合、出力側では、同じデータ D1 が D2 より先に FIFO から出なければならないと言えます。

これを PSL で表現するには、いくつかの補助信号が必要です:542 、 557 、 562 、および 574 .これらの信号はリセット時にクリアされ、D1 または D2 が FIFO に出入りするたびにアサートされます。一度アサートされると、これらの信号はアサートされたままになります。

したがって、FIFO の順序付けプロパティを 2 つの部分で表現します。最初に 仮定 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;

ここでは、他の 2 つのシグナル 583 を参照しています。 と 597 .これらには、データ値 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;

606 属性は正式な検証ツールによって認識されます。これは、ツールが任意の定数値をその場所に挿入できることを示しています。

上記で、FIFO のプロパティを指定しました。

フォーマル検証の実行

正式な検証ツールを実際に実行する前に、小さなスクリプト 611 を書く必要があります。 :

[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

セクション 625 Bounded Model Checking を行いたいと述べています。セクション 630 BMC を 10 クロック サイクル実行するように指定します。デフォルトは 20 です。セクション 648 いくつかの異なるソルバーからどれを使用するかを選択します。特定の設計に応じて、さまざまな可能なエンジンの実行速度に違いが生じる可能性があります。今のところ、この値はそのままにしておきます。

657 セクションは興味深い部分です。ここでは、VHDL 標準 (2008)、ジェネリックの値、処理するファイル、最上位エンティティの名前を指定します。最後に、669 セクションにファイル名が再び含まれています。

このスクリプトの準備ができたら、次のコマンドを使用して実際の正式な検証を実行できます:

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

正式な検証ツールを実行すると、無礼なステートメントで終わります:

[axi_fifo_bmc] DONE (PASS, rc=0)

これは、指定したすべてのプロパティが、最大 10 クロック サイクルのすべての任意の入力で満たされることを意味します。深さを増やすと、ソルバーの実行時間が長くなります。ただし、深さは FIFO の深さよりも大きいことに注意してください。つまり、BMC は一部の入力シーケンスで FIFO がいっぱいになる状況に遭遇します。たとえば 5 クロック サイクルのみを選択した場合、正式な検証で FIFO がいっぱいになることはなく、それに関連するバグも検出されません。

すべてのプロパティが満たされていることを証明できます 誘導証明を使用してクロックサイクル。ただし、そのためには、プロパティを記述する作業がさらに必要になります。課題は、これまでに いくつか を書いただけです。 プロパティ。しかし誘導のために、all を指定する必要があります プロパティ (または少なくとも十分な数)。それにはかなりの時間がかかるため、代わりに、自信を高めるための別の戦略について説明します。

突然変異

これで 673 のプロパティのいくつかを説明しました。 モジュールは満たす必要があり、ツールはそれらのプロパティをすばやく確認します。つまり、それらが満たされていることを証明します。しかし、まだ不安な気持ちが残るかもしれません:バグは本当にないのでしょうか? 686 のすべてのプロパティを本当に表現したか モジュール?

これらの質問に答え、指定されたプロパティの完全性に対する信頼を高めるために、ミューテーションと呼ばれる手法を適用できます。 :意図的に実装に小さな変更を加えます。つまり、意図的にバグを導入し、正式な検証でバグがキャッチされるかどうかを確認します!

そのような変更の 1 つは、690 を制御するロジックの一部を削除することです。 信号。たとえば、次の 3 行をコメント アウトできます。

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 で 707 信号はゼロになるはずですが、そうではありません。失敗するアサーションは 50 ns で、ここで 719 高いままですが、724 信号が変化し、データが重複していることを示します。 733 のため、この特定のトレースでは重複データは実際には送信されませんでした。 は 40 ns と低いですが、正式な検証ではバグが検出されます。

カバー ステートメント

最後に、正式な検証ツールの別のアプリケーションに目を向けましょう:カバー ステートメントです。 cover ステートメントの目的は、特定のプロパティを満たす一連の入力があるかどうかを確認することです。 FIFO を扱っているので、FIFO を完全に満たしてから、再び空にできるかどうかを見てみましょう。これは、1 つのカバー ステートメントで表現できます。

f_full_to_empty : cover {
   rst = '1';
   rst = '0'[*];
   rst = '0' and count = ram_depth-1;
   rst = '0'[*];
   rst = '0' and count = 0};

それはかなりの口いっぱいです！ 748 内のセミコロンに注意してください .読みやすくするために、各セクションを別の行に配置しました。このカバー ステートメントは次のように書かれています:条件を満たす一連の入力を探します:

• リセットは 1 クロック サイクルの間アサートされます。
• 任意の数のクロック サイクル (リセットがアサートされていない場合) が通過する可能性があります。
• リセットがアサートされず、FIFO がフルの 1 クロック サイクル
• 任意の数のクロック サイクル (リセットがアサートされていない場合) が通過する可能性があります。
• リセットがアサートされず、FIFO が空の 1 クロック サイクル

したがって、構文 759 前の条件を (0 回以上) 繰り返すことを意味します。 3 行目で、条件 765 を削除できました。 779 の前 .結果は同じになります。その理由は、正式な検証者が最短を見つけようとするからです。 FIFO を満たしている間にリセットをアサートすると、それが遅延するだけです。ただし、5 行目で FIFO を空にするときは、リセットがアサートされないことが不可欠です。

正式なベリファイアを今すぐ実行するには、スクリプト 780 を少し変更する必要があります。 .上部のセクションを次のように置き換えます:

[tasks]
bmc
cover

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

これでソルバーは BMC を実行し、次にカバー解析を実行します。出力には、次の 2 行が表示されます。

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

これは、15 クロック サイクルのシーケンスで実際にカバー ステートメントを満たすことができ、ソルバーがこのカバー ステートメント専用の波形を生成したことを意味します。

ここでは、80 ns で FIFO がいっぱいになり、791 になっていることがわかります。 アサート解除されます。そして 150 ns で FIFO は空になり、809 アサート解除されます。 816 という 30 ns から 80 ns の期間中の方法に注意してください。 低く保たれます。これは、FIFO がいっぱいになるようにするために必要です。

条件 827 を置き換えると 837 で 、カバーステートメントを満たすことができません。その後、ツールはエラーを報告します。

Unreached cover statement at i_axi_fifo.f_full_to_empty.

したがって、エラー メッセージには、失敗した cover ステートメントのラベルが含まれています。これが、ラベルが便利な理由の 1 つです。上記のエラーは、FIFO が 847 を保持できないことを示していると解釈します。 要素数。これは、元の AXI FIFO ブログ投稿に記載されているとおりです。

ここからどこへ行く

• PSL 言語の入門書
• 正式な検証の概要
• 正式な検証を開始するための一連の小さなビデオ
• 形式検証に関するブログ
• フォーマル検証のより高度なトピックを取り上げた一連の記事
• フォーマル検証を使用した小さな例のコレクション