360 MV™ のFormalDoublePASS™ 完全性達成手法
完全性を達成するための手法、FormalDoublePass™は、検証の計画から真の機能サインオフ達成まで設計者を支援します。 この手法は、以下の4つの検証段階を通じて360 MVの機能をフルに活用し、エラーのないモジュールおよびIPを効率的に完成するための手法です。FormalDoublePASS™ を構成する4つの段階
-
検証のプランニング
ユーザーは全体の検証タスクを、仕様、設計のトランザクション ビュー、およびツールが支援するコードレビュー プロセスに従ってサブタスクに分割します。 -
設計のコンディショニング
ユーザーは自動的に生成された詳細な設計一貫性チェックを使って、RTLから一般的なコーディング エラーを迅速に取り除きます。 -
プロパティ開発
ユーザーはプロパティ開発環境を用い、仕様に準拠した、トランザクションレベルのプロパティを使って選択されたコードを段階的に記述し、検証します。 デバッグ／診断環境により、ユーザーはRTL、プロパティ、またはもとの仕様に含まれるエラーの原因を迅速に特定できます。 -
完全なプロパティセットの開発
自動化された完全性解析を用いて、 すべての 検証の穴を体系的に検出します。 詳細なデバッグおよび診断情報を用いて、ユーザーはこれらの穴をふさぐためのプロパティを開発し、証明していきます。 この完全性解析により、プロパティが完全であると確認されると、ユーザーは検証が完了したことを確実に知ることができます。 この時点で、True Functional Sign-off（真の機能サインオフ）が達成されたことになります。
True Functional Sign-Off達成により以下が得られます：
- RTLには意図しない、予期しない、あるいは検証されていない動作が含まれない − エラーのない動作が保証される
- エラー、抜けのない仕様
- 証明済みの、仕様に準拠したプロパティの完全なセット
- あらゆるターゲット設計に対する正しい統合を可能にする、統合条件の完全なセット