フォーマル検証　等価性チェック eCheck / sCheck

Synplifyとのインタフェースについて

等価性検証ツールを用いた、シンプリシティとProver社によるロジック検証フロー

パフォーマンス向上の為に論理合成がデザイン変換
−有限ステートマシンの再エンコーディング、ポート方向の変更、レジスタのマージや複製− を行った場合でも、Verification Interchange Formmat（.vif）を使えば、面倒なセットアップファイルは自動生成されます。

背景

等価性検証ツールは、ASICの開発フローにおいて論理合成結果お検証ツールなどに
近年利用されてきています。
一方、FPGAの開発フローにおいては、より複雑なデザイン変換が発生し、又そのデザイン変換を処理するための設定が複雑で、等価性検証ツールの恩恵を受ける事が難しい状況でした。

信頼するに足るファンクショナルクロージャ

Prover社とシンプリシティ社は共同で、この問題を解決するべくFPGA開発フローを提案します。すなわち、「設定ファイルの自動生成」です。
論理合成が終わると、Prover社等価性チェックツールeCheckのセットアップファイルが自動生成されます。セットアップファイルには、論理合成において施されたデザイン変換に関する情報、すなわち有限ステートマシンの再エンコーディング、ポート方向の変更、レジスタのマージや複製、等がリストされています。
一般的に複雑な、等価性検証ツールに教えなければならないデザイン変換情報は、eCheckのセットアップファイルとして自動生成されますので、等価性検証ツールを容易に FPGA開発フローに組み込む事ができます。

ファインクショナルクロージャの重要性

スピード向上や面積縮小などのパフォーマンス向上の為、先進的な論理合成ツールは入力RTLに対し、デザイン変換や最適化を施します。また、対象となるFPGAは年々大規模化へ向かっています。これらの背景をふまえ、論理合成前後のデザインに対し等価性検証ツールを適用する事は大変重要です。以下は、論理等価性が重要になる一例です。

• 医用、軍事、組込システム等
  バグの混入によるリコールやリワークは甚大な損害につながります。
• プロトタイプFPGA
  試作となるFPGAにおいて、FPGAに展開されているロジックがRTLと一致している 事は大変重要です。「ゴールデンRTL−プロトタイプFPGA」間に等価性が保証されない限り、量産を ASICへ移行する場合などでは、いくらASIC開発工程において等価性検証を行ってもリワークの可能性をはらんでいることになります。
• リターゲット
  ゴールデンRTLモデルが確立されていれば、リターゲットや論理合成のオプション 変更を試す際にも、等価性検証ツールで高速にトレードオフが検討できます。

強力なマッピングエンジン

ほとんどの場合デフォルト設定でマッピングが実現されますが、万一デフォルトの設定で失敗した場合でも、正規化表現によるユーザ定義のマッピングルール等でマッピングを指定することもできます。

効率的なデバック環境

不一致が発生した場合には、反例となるテストベクタを表示した回路図やログによる、効率的なデバック環境を提供します。

 

資料

日本語eCheck2.1x3.PDFへのリンク
eCheck 日本語スライドへのリンク