フォーマル検証・プロパティ チェック　 VerityCheck

クロックドメインの検証に！
PSL/Sugarによるプロパティ検証に！
コード品質向上のlintツールに！

BluePearlは機能検証を効率化します

大規模回路のデザインプロパティを、テストベンチを使用することなく高速に検証します

フォーマルバリデーションを体験してください！

設計したRTLデザインは仕様を満足しているでしょうか？
Blue Pearl Software社の製品群は、検証工数を劇的に削減し、ハイパフォーマンスで高性能なデザインバリデーションソリューションを提供います。

使い易く便利なlint（文法チェック機能）に、強力なフォーマルバリデーション機能

BluePearlプロパティチェッカはデザイン検証をよりシンプルにし、検証効率を上げる確信的な フォーマル検証ツールです。
操作性に優れており、ほとんどの設定はGUI上のチェックボックスで設定できます。また、バッチ処理に適したコマンドラインによるオペレーションにも対応しています。伝統的な手法であるルールチェッキング／lintツールとフォーマル検証技術とが同じプログラムパッケージとして提供されており、同じGUIでlintやプロパティ検証を行うことができます。 一般的に必要とされる検証項目が選択可能なチェック項目として用意されているので、それら チェック項目を選択することで簡単に検証を始めることができます。

デザインプロパティを自動検出

BluePearlは、RTLを素早く解析してデザインプロパティを自動検出します。
自動検出されるプロパティには「３ステートバスの競合」、「フローティングバスの検出」、「レジスタのセット１−リセット競合」等があります（後述）。また、特定ネットやグループネットのワンホット定義のチェックもできます。
BluePearlはこれらのプロパティを、洗練されたフォーマルバリデーション技術を用いて検証します。シンボリックシミュレーションを用いてステートスペース（状態空間）を徹底的に探索し、制約条件を加味しながら、入力ベクタを必要とせずにプロパティ違反を検出します。制約条件は、GUIでもテキストベースでも与えることができます。プロパティ違反を正確にフィードバックし、デバック工数を短縮します。RTLコードのエラー箇所を明示し、プロパティ違反を証明する反例のテストベクタを自動生成します。

ユーザ定義のプロパティを検証

ユーザ定義のプロパティを作成することも可能です。
ユーザ定義のプロパティとは、例えば、「指定サイクル数内にリクエスト信号が認識される」、「指定した２信号は相互に排他的関係にある」などです。 また、サイクルベースの検証技術に的確な制約を与える事で検証すべきステートを絞り込み、これまでのモデルチェックツールと比較して対応可能な設計サイズを広げることができます。
プロパティ記述言語として、独自言語の他に、AccelleraのPSL/Sugarにも対応しています。

シミュレーション前に信号のレーシングを検出

信号の競合は重大なデザインエラーとなる可能性が大きく、十分に検証する必要があります。 一方、従来のシミュレーションを使用した検証で信号競合を検証するには多くの工数と時間を必要とします。BluePearlでは、静的検証（シミュレーションを行わない、入力パタンを用意する必要がない）により、これら信号競合発生箇所の検証を行う事ができます。BluePearlは、write−write、read−write、組み合わせループの競合等の競合コンディションを認識し、原因となるソースコードを指摘します。

クロックドメインの同期化チェック

BluePearlは、複数のクロックドメインデザインを認識し、クロックドメイン間を渡るデータの同期
性を検証します。ダブルレジスタバッファリング、メモリ／レジスタファイル、及びカスタマイズされた同期化構成を認識します。クロックドメイン間における同期化構成に問題がある場合、これをレポートします。

クロックドメイン同期化検証レポート例

【クロックドメインチェック 】

• クロックドメイン間を渡る信号を検出
• クロックドメイン間でデータが同期化されているかのチェック
• 同期化回路が構成されているかのチェック

多くのプロパティを迅速に検証

BluePearlでは、以下のようなプロパティをチェックすることができます：

【信号競合検出 】

• Write-Write
• Read-Write
• Latch-Latch
• 組み合わせループ
• ゲーテッドクロックによる競合

【デザインの再利用性】

• コーディングスタイル
• リユースメソドロジマニュアル準拠（RMM）
• Semiconductor Reuse Standard準拠（SRS）

【論理合成前のチェック】

• シミュレーション−論理合成の結果不一致
• 不必要なラッチの生成

【テスタビリティのチェック 】

• RTLを対象にATPGが問題なく行われるかのチェック
• ゲーテッドクロックの検出
• 非同期クロック
• 非同期セット／リセット

【回路の構造チェック 】

• 不定の検出
• 冗長回路の検出
• 競合アサイン
• レンジ違反
• リセットのかからないフリップフロップの検出

サポート言語

Verilog-HDL

サポートプラットフォーム

Solaris、Linux、Windows2000/XP

ご評価用プログラム

是非一度BluePearlを使用してみてください！
BluePearlのHPから、評価用のプログラムをダウンロードすることができます。

http://www.bluepearlsoftware.com/html/2_evaluation.html
あるいは、インターリンクまでご要求ください。

E-mail: ilink_sales@ilink.co.jp