形式的等価性チェック

形式的等価性チェックプロセスは、電子設計自動化(EDA)の一部であり、デジタル 集積回路の開発中に一般的に使用され、回路設計の 2 つの表現がまったく同じ動作を示すことを正式に証明します。

一般に、機能的等価性には、異なる抽象化レベルとタイミング詳細のさまざまな粒度間の比較をカバーする幅広い定義が可能です。

• 最も一般的なアプローチは、マシン等価性の問題を考慮することです。これは、2 つの同期設計仕様が、クロックごとに、任意の有効な入力信号シーケンスに対してまったく同じ出力信号シーケンスを生成する場合に、機能的に同等であると定義するものです。
• マイクロプロセッサの設計者は、等価性チェックを使用して、命令セットアーキテクチャ (ISA)に指定された関数をレジスタ転送レベル(RTL) 実装と比較し、両方のモデルで実行されるすべてのプログラムがメインメモリの内容に対して同一の更新を引き起こすことを確認します。これは、より一般的な問題です。
• システム設計フローでは、 SystemCで記述されたトランザクション レベル モデル (TLM)とそれに対応する RTL 仕様との比較が必要です。このようなチェックは、システム オン チップ (SoC) 設計環境でますます重要になっています。

デジタル チップのレジスタ転送レベル (RTL) の動作は、通常、 Verilog や VHDL などのハードウェア記述言語で記述されます。この記述は、どのクロックサイクルでどの操作がどのハードウェアによって実行されるかを詳細に記述する、ゴールデン リファレンス モデルです。ロジック設計者がシミュレーションやその他の検証方法によってレジスタ転送記述を検証すると、通常、その設計はロジック合成ツールによってネットリストに変換されます。同等性と機能の正確性とを混同しないでください。機能の正確性は、機能検証によって決定する必要があります。

通常、初期のネットリストは、最適化、テスト容易化設計(DFT) 構造の追加など、いくつかの変換を経てから、物理レイアウトへのロジック要素の配置の基礎として使用されます。現代の物理設計ソフトウェアは、ネットリストに大幅な変更 (ロジック要素を、より高いまたはより低い駆動力および/または面積を持つ同等の類似要素に置き換えるなど) を加えることもあります。非常に複雑で複数のステップから成る手順のすべてのステップを通じて、元のコードで記述された元の機能と動作を維持する必要があります。最終的なテープアウトがデジタル チップから作成されるときには、多くの異なる EDA プログラムと、場合によってはいくつかの手動編集によって、ネットリストが変更されていることになります。

理論上、ロジック合成ツールは、最初のネットリストがRTL ソース コードと論理的に同等であることを保証します。また、理論上、プロセスの後半でネットリストに変更を加えるすべてのプログラムも、これらの変更が以前のバージョンと論理的に同等であることを保証します。

実際には、プログラムにはバグがあり、RTL から最終的なテープアウト ネットリストまでのすべてのステップがエラーなしで実行されたと想定するのは大きなリスクです。また、現実には、設計者がネットリストに手動で変更を加えることは一般的であり、これは一般にエンジニアリング変更指示(ECO) と呼ばれ、これによって大きなエラー要因が追加されます。したがって、間違いがなかったと盲目的に想定するのではなく、ネットリストの最終バージョンと設計の元の記述 (ゴールデン リファレンス モデル) の論理的等価性をチェックする検証ステップが必要です。

歴史的に、同等性をチェックする 1 つの方法は、RTL の正確さを検証するために開発されたテスト ケースを、最終的なネットリストを使用して再シミュレートすることでした。このプロセスは、ゲート レベルロジック シミュレーションと呼ばれます。ただし、この方法の問題点は、チェックの品質がテスト ケースの品質と同程度しかないことです。また、ゲート レベル シミュレーションは実行速度が遅いことで有名であり、デジタル設計のサイズが指数関数的に増加し続ける中で、これは大きな問題となります。

これを解決する別の方法は、RTL コードとそこから合成されたネットリストがすべての (関連する) ケースでまったく同じ動作をすることを正式に証明することです。このプロセスは形式的等価性チェックと呼ばれ、形式的検証というより広い分野で研究されている問題です。

正式な同等性チェックは、設計の任意の 2 つの表現 (RTL <> ネットリスト、ネットリスト <> ネットリスト、または RTL <> RTL) の間で実行できますが、後者は最初の 2 つに比べてまれです。通常、正式な同等性チェック ツールは、2 つの表現の間に違いが存在するポイントを非常に正確に示します。

等価性チェック プログラムにおけるブール推論に使用される基本的なテクノロジは 2 つあります。

• 二分決定図(BDD): ブール関数の推論をサポートするために設計された特殊なデータ構造。BDD は、その効率性と汎用性から非常に人気が高まっています。
• 連言標準形の充足可能性: SATソルバーは、命題式の変数への割り当てが、その割り当てが存在する場合に、その割り当てを満たすものを返します。ほぼすべてのブール推論問題は、SAT 問題として表現できます。

EDAのロジック等価性チェック ( LEC ) 分野の主な製品は次のとおりです。

• Mentor GraphicsのFormalPro
• メンターグラフィックスのQuesta SLEC
• ケイデンスのコンフォーマル
• ケイデンスのジャスパー
• Synopsysによる形式
• SynopsysによるVC フォーマル
• OneSpin Solutions の360 EC
• ATECによるATEC

• リタイムされた回路の等価性チェック: ロジックをレジスタの一方側から他方側に移動すると便利な場合がありますが、これによりチェックの問題が複雑になります。
• 順次等価性チェック: 場合によっては、2 つのマシンが組み合わせレベルではまったく異なりますが、同じ入力が与えられた場合は同じ出力を返す必要があります。典型的な例は、状態のエンコードが異なる 2 つの同一の状態マシンです。これは組み合わせ問題に還元できないため、より一般的な手法が必要です。
• ソフトウェア プログラムの同等性、つまり N 個の入力を受け取り、M 個の出力を生成する 2 つの明確に定義されたプログラムが同等であるかどうかのチェック: 概念的には、ソフトウェアをステート マシンに変換できます (これは、コンピューターとそのメモリが非常に大きなステート マシンを形成するため、コンパイラの組み合わせによって行われます)。次に、理論上は、さまざまな形式のプロパティ チェックによって、同じ出力が生成されることを保証できます。この問題は、2 つのプログラムの出力が異なる時間に現れる可能性があるため、順次同等性チェックよりもさらに困難です。ただし、これは可能であり、研究者が取り組んでいます。

• 形式手法

• 『Electronic Design Automation For Integrated Circuits Handbook』、Lavagno、Martin、Scheffer 著、ISBN  0-8493-3096-3この分野の調査。この記事は、Fabio Somenzi と Andreas Kuehlmann 著、第 2 巻第 4 章「Equivalence Checking 」から許可を得て抜粋したものです。
• RE Bryant、「ブール関数操作のためのグラフベースアルゴリズム」、IEEE Transactions on Computers.、C-35、pp. 677–691、1986。BDD に関するオリジナルの参考文献。
• RTL モデルの順次同等性チェック。Nikhil Sharma、Gagan Hasteer、Venkat Krishnaswamy。EE Times。

• CADP – 非同期設計のための等価性チェックツールを提供します
• OneSpin 360 EC-FPGA – RTL コードから最終ネットリストまでの FPGA 合成の機能的正確性