等価性検証とは、リファレンス・デザイン（ゴールデン・デザイン）と変更後のデザインとの論理等価性を形式論理学的に検証するための、フォーマル検証手法のひとつです。比較する両方のデザインとも、合成可能な HDL またはゲート・レベル・ネットリストである必要があります。等価性検証手法では、ベクタ、スティミュラス、またはテストベンチを必要としません。等価性検証手法は、HDLデザイン（リファレンスとなるデザイン）を論理合成によりゲートレベル・ネットリストへ変換するなど、あるデザインを別の抽象度のデザインへ変換した際に使用されます。この手法はゲート・レベル・タイミング・シミュレーションの完全な代替手法ではありませんが、ゲート・レベル・ネットリストを使用したシミュレーションよりも、迅速にくまなく HDL デザインが正しく変換されたかどうかを検証できます。このデザイン例では、アルテラの Quartus® II ソフトウェアで生成したフィッティング後のネットリスト・ファイルを使用して、Cadence Encounter Conformal ツールでの等価性検証フローを示します。
ここで使用するデザイン例では、RTLレベルのHDL と Quartus II ソフトウェアで生成したフィッティング後のネットリストとの間で、等価性検証を実行します。等価性検証ツールを実行するための Quartus II ソフトウェアのセットアップ方法や、等価性検証ツールを実行するうえで必要な Quartus II ソフトウェアからの出力ファイルについて説明します。
この例では、以下を実行します。
- 用意してあるデザインを Quartus II ソフトウェアで開く
- 等価性検証に必要なファイルを生成するための Quartus II ソフトウェアの設定
- 必要な設定を反映したプロジェクトをコンパイル
- 等価性検証で使用する出力ファイルの確認
- 等価性検証の実行
ここでのデザイン例は、Red Hat Linux マシンで動作する Quartus II ソフトウェア・バージョン 6.0 サービス・パック 1 と Cadence Encounter Conformal ツール・バージョン 06.10-p100（2006 年 5 月 25 日）の使用を想定しています。同じデザイン例を Windows または Sun Solaris オペレーティング・システムを搭載したホストで動作中の、Quartus II ソフトウェアおよび Cadence Encounter Conformal ツールで使用することもできます。
このデザイン例は、シンプルな 8 ビット乗算器ブロックと Stratix® II デバイスに実装された PLL （phase-locked loop） ブロックで構成されています。フォーマル検証に必要なすべてのライブラリは Quartus II ソフトウェアにより提供されます。このデザイン例を使用するには、以下のステップを実行します。
- 乗算器デザインに必要な Quartus II アーカイブ・ファイル （拡張子 .qar） をダウンロードします。
- Linux システムのコマンド・プロンプトで
quartus formal-verification.qarと入力して、Enter を押します。 - Quartus II ソフトウェアが起動し、Restore Archived Project ダイアログ・ボックスが表示されます。Restore Archived Project ダイアログ・ボックスでは、復元されたプロジェクトを展開するディレクトリを指定して OK をクリックします。
- Assignments メニューで Settings を選択します。
- Settings ダイアログ・ボックスの EDA Tool Settings ページで、Formal Verification の下の Conformal LEC を選択します。
- Settings ダイアログ・ボックスの Incremental Compilation ページで、Full Incremental Compilation がオンになっていることを確認します。
- OK をクリックして、Settings ダイアログ・ボックスを閉じます。
- デザインをコンパイルします。コンパイルが終了すると、<project_dir>/fv/conformal に multiplier.vo が作成されます。これはフィッティング後に Quartus II ソフトウェアで生成されるネットリストで、Cadence Encounter Conformal ツールによる等価性検証で使用します。また、Quartus II ソフトウェアは <project_dir>/fv/conformal に、Cadence Encounter Conformal ツールで使用するスクリプトを生成します。
- Quartus II ソフトウェアを閉じます。
- Linux コマンド・プロンプトで、
cd <project_dir>/fv/conformalと入力して、<project_dir>/fv/conformal ディレクトリに移動します。 lec -dofile multiplier.ctcと入力して、Cadence Encounter Conformal ソフトウェアを起動します。このコマンドは Cadence Encounter Conformal ツールを起動し、HDL デザイン・ファイル （リファレンス・デザイン） とフィッティング後に Quartus II ソフトウェアで生成されたネットリストとの間で等価性検証を実行します。Cadence Encounter Conformal ツールで結果を確認します。
Windows マシンで動作中の Quartus II ソフトウェア、および UNIX/Linux マシンで動作中の Cadence Encounter Conformal ツールを使用してプロジェクトをコンパイルした場合、そのデザイン例を実行するには Quartus II ソフトウェアで生成されたスクリプトを編集しなければならないことがあります。
Quartus II ソフトウェアおよび Cadence Encounter Conformal ツールを使用した等価性検証の実行について詳しくは、「Quartus II ハンドブック volume 3」の Cadence Encounter Conformal Support の章（PDF）を参照してください。
