UPGRADE YOUR BROWSER

We have detected your current browser version is not the latest one. Xilinx.com uses the latest web technologies to bring you the best online experience possible. Please upgrade to a Xilinx.com supported browser:Chrome, Firefox, Internet Explorer 11, Safari. Thank you!

AR# 25007

フォーマル検証 - よく寄せられる質問 (FAQ)

説明

このアンサーには、フォーマル検証に関してよく寄せられる質問 (FAQ) がリストされています。

 

質問 1) ザイリンクスでは等価チェックおよびモデル チェックをサポートしていますか。

質問 2) フォーマル検証とは何ですか。

質問 3) ザイリンクスで等価チェックをサポートしているのはなぜですか。

質問 4) モデル チェックはいつサポートされるようになりますか。

質問 5) 等価チェックはシミュレーションに置き換わるものですか。

質問 6) 等価チェックはいつ使用すべきですか。

質問 7) ザイリンクスでは XST 後のフローをサポートしていますか。

質問 8) 等価チェックを使用するとどのような利点がありますか。

質問 9) ザイリンクスがサポートするベンダーを教えてください。

質問 10) サポートに関する問題はどこに連絡すればよいですか。

質問 11) フローを説明しているザイリンクス アプリケーション ノートはありますか。

質問 12) フローはすべての言語で機能しますか。

質問 13) サポートされているプラットフォームを教えてください。

質問 14) 等価チェックを使用して FPGA を ASIC に変換する方法を教えてください。

質問 15) ザイリンクスが提供しているライブラリを教えてください。

質問 16) サポートされるフォーマル検証ツールのフォーマル検証ライブラリの入手先を教えてください。

ソリューション

質問 1) ザイリンクスでは等価チェックおよびモデル チェックをサポートしていますか。

回答 1) 現在の ISE ソフトウェアでは、等価チェックのみがサポートされます。



質問 2) フォーマル検証とは何ですか。

回答 2) フォーマル検証はアルゴリズム ベースのアプローチでロジック検証を実行し、デザインに関する論理的プロパティを数多く提供します。

通常、次の 2 つのタイプのフォーマル検証があります。

等価チェック

抽象化レベルが同じまたは異なる、論理的には同等 2 つのデザインを検証します (たとえば、RTL と RTL、RTL とゲート、ゲートとゲートなど)。 

等価チェックは、デザイン インプリメンテーションの検証に使用されます。

モデル チェック

インプリメンテーションがデザインの特性を満たすかどうかを検証します。 

モデル チェックは、機能的な問題点を検出するため、デザイン作成の初期段階で実行されます。



質問 3) ザイリンクスで等価チェックをサポートしているのはなぜですか。

回答 3) デバイスの大型化、デザインの複雑化に伴い、論理シミュレーションにかかる時間は、テストベンチ生成およびシミュレーション実行時間の両方で非常に長くなってきています。

フォーマル検証はランタイムが短く、機能を完全に検証するので有益です。

また、フォーマル検証は ASIC のデザイン環境で実績のあるテクノロジ/フローです。 

多くの ASIC 設計者がデザインに FPGA を使用するようになっており、フォーマル検証はデザインの重要なフローとなっています。



質問 4) モデル チェックはいつサポートされるようになりますか。 

回答 4) モデル チェックは比較的新しい技術であり、また各ベンダが独自のプロパティ記述言語を使用しているため、カスタマによりまだそれほど採用されていません。

デザイン プロパティを記述する 1 つの標準言語が確立された場合、このテクノロジの採用は増加する可能性があります。 

ザイリンクスでは、カスタマの要望に基づき、モデル チェックのサポートを検討する予定です。


質問 5) 等価チェックはシミュレーションに置き換わるものですか。 

回答 5) 等価チェックは論理シミュレーションを補足するものです。

数百万ゲートのデザインでは、シミュレーションの実行に数日または数週間かかる場合があるため、等価チェックが唯一の実行可能なソリューションです。

また、シミュレーションではデザイン全体が完全に網羅されるわけではありません。等価チェックでは、シミュレーションよりも短い時間で、テスト ベクタを使用せずにデザイン全体を網羅できます。


質問 6) 等価チェックはいつ使用すべきですか。

回答 6) 等価チェックは、FPGA インプリメンテーション フロー全体で使用してください。

デザインの再最適化、合成、および配置配線の結果を、検証済みの RTL モデルに対して検証できます。


質問 7) ザイリンクスでは XST 後のフローをサポートしていますか。 

回答 7) いいえ。


質問 8) 等価チェックを使用するとどのような利点がありますか。 

回答 8) 等価チェックを使用すると、デザインをより短時間で検証できます。

最終ネットリストの機能が検証済みの RTL デザイン仕様と一致していることを確認するのに役立ちます。

また、問題の特定およびデバッグも効率的に実行できます。


質問 9) ザイリンクスがサポートするベンダーを教えてください。 

回答 9) ISE Design Suite では次のベンダーがサポートされています。

Synopsys Formality:

http://www.synopsys.com

Cadence Conformal LEC:

http://www.cadence.com/

Mentor Graphics Formal Pro (ベンダーによる直接サポート):

http://www.mentor.com/

Vivado では、Cadence Encounter Conformal で 2018.1 から OneSpin がサポートされています。


質問 10) サポートに関する問題はどこに連絡すればよいですか。 

回答 10) ツールおよびフローに関する問題:

Synopsys Formality: 

http://solvnet.synopsys.com

Cadence 社 Conformal: 

http://www.cadence.com/support/

Prover eCheck:

http://www.prover.com/contact/

ライブラリの問題:

ザイリンクスのサポート: 

https://japan.xilinx.com/support.html#serviceportal


質問 11) フローを説明しているザイリンクス アプリケーション ノートはありますか。 

回答 11) フォーマル検証に関するザイリンクス アプリケーション ノートは、すべて廃盤になっています。

フォーマル検証に関する情報は、次を参照してください。

Cadence Conformal: (Xilinx Answer 20617)

Prover eCheck: (Xilinx Answer 20685)


質問 12) フローはすべての言語で機能しますか。  

回答 12) RTL レベル: VHDL および Verilog の両方がサポートされます。詳細は、フォーマル検証ベンダーにお問い合わせください。

ゲート レベル: ザイリンクスでは Verilog フローのみをサポートしいています。


質問 13) サポートされているプラットフォームを教えてください。  

回答 13) プラットフォーム サポートは、次のとおりです。

Synopsys Formality

Sun OS Unix*: サポートあり

Linux Enterprise Edition*: サポートあり

Windows XP/2000*: サポートなし

Cadence 社 Conformal

Sun OS Unix*: サポートあり

Linux Enterprise Edition*: サポートあり

Windows XP/2000*: サポートなし

Prover 社 eCheck

Sun OS Unix*: サポートあり

Linux Enterprise Edition*: サポートあり

Windows XP/2000*: サポートあり

* ザイリンクス ISE でサポートされるバージョンのみ


質問 14) 等価チェックを使用して FPGA を ASIC に変換する方法を教えてください。  

回答 14) 次の 2 つの方法を使用して、FPGA を ASIC に変換できます。

  • RTL からゲート: ソース RTL が FPGA と ASIC で同じ場合に使用します。
  • FPGA ゲートから ASIC ゲート: FPGA のゲート レベル ネットリストを ASIC のゲート レベル ネットリストと比較する場合に使用します。

注記: これらのフローの詳細は、フォーマル検証ベンダーにお問い合わせください。


質問 15) ザイリンクスが提供しているライブラリを教えてください。  

回答 15) ザイリンクスでは、フォーマル検証用に次の 2 つのライブラリを提供しています。

  • UNISIM ライブラリ* - RTL インスタンシエーション用にテクノロジー別にセルをインスタンシエートしたデザインに使用します。
  • SimPrim ライブラリ* - NGDBuild 後および配置配線後のネットリストに使用します。

* これらのライブラリは、ザイリンクスが提供するシミュレーション ライブラリとは異なります。


質問 16) サポートされるフォーマル検証ツールのフォーマル検証ライブラリの入手先を教えてください。  

回答 16) 古い ISE リリースの場合、次のような CAE ベンダー ライブラリが提供されています。

http://japan.xilinx.com/support/download/index.htm

ISE Design Suite の 12.1 リリースより、ライブラリはこのソフトウェアで使用できるようになっています。

ファイルは、$XILINX/verilog/xeclib にあります。

Vivado で配布されるライブラリは $XILINX_VIVADO/data/verilog/src/xeclib/ にあります。

AR# 25007
日付 06/08/2018
ステータス アクティブ
種類 一般
ツール
  • ISE Design Suite
  • Vivado Design Suite
このページをブックマークに追加