メンター・グラフィックスのQuesta機能検証プラットフォーム、広範なフォーマル検証機能を提供
2012/10/19
シーメンスEDAジャパン株式会社
メンター・グラフィックス・コーポレーション（本社: 米国オレゴン州、以下メンター・グラフィックス）は、大多数の機能検証ユーザが簡単に包括的なフォーマル検証解析を実行できる新しいフォーマル技術を、同社のQuesta®機能検証プラットフォームに搭載したことを発表しました。最新技術であるQuesta AutoCheckはフォーマルチェック解析を完全自動化し、Questa CoverCheckは100%のコードカバレッジを達成します。さらに、今回発表されたQuestaプラットフォームにはクロックドメイン・クロッシング（CDC）機能も追加されています。
テスト・スティミュラスを指定せずに設計上のあらゆる機能的な振る舞いを網羅的に解析できるフォーマル検証は、シミュレーション用テストベンチを作成する前の設計サイクルの早期段階での検証を可能にする手法です。しかし、従来のフォーマル検証で謳われていた内容は、熟練したフォーマル解析エンジニアがいる検証チームでなければ実現できず、その達成は大きな労力を要するものでした。Questaは、ボタンを押すだけで誰でも簡単に操作できるパワフルなAutoCheckによる完全自動化されたフォーマルチェックから、より高度なユーザを対象としたアサーションコードのカスタマイズによるプロパティ・チェック機能まで、多岐にわたるアプリケーションを揃えることにより、これまでのフォーマル検証を一変させました。これは、標準的なコンパイル機能やユーザ・インタフェース、UCDB（Unified Coverage Database）にシミュレーション技術およびフォーマル技術をシームレスに融合させた広範な検証ソリューションです。
■Questa CoverCheckによる100%のコードカバレッジ
Questa CoverCheckは、コードのカバレッジ・クロージャを高速化する技術です。カバレッジ・クロージャを達成するには通常、無視できるカバレッジ・ホールかどうかをマニュアルで確認し、無視できないカバレッジ・ホールに対してはシミュレーション用のテストコードを手作業で記述しなければならないため、何週間もの作業が必要です。Questa CoverCheckであれば、専門のエンジニアでなくても、フォーマル手法を活用して、カバレッジ・クロージャを達成できるビンと達成できないビンを自動的に識別できます。その結果、コードカバレッジのサインオフにかかる時間を大幅に短縮でき、スケジュールの見通しを立てやすくなります。また、コードカバレッジのビンが誤って無視されて検証プロセスから漏れてしまうというミスを防止することにより、高い検証品質を確保できます。
■主流ユーザ向けのAutoCheckを搭載したQuesta Formal
AutoCheckは、振る舞いのシーケンスをチェックする強力なフォーマル検証ツールの処理に先立ってRTL設計を解析し、自動的にアサーションを合成します。AutoCheckを使用すると、テストベンチやアサーションをユーザが記述する必要がなく、一般的な機能エラーが設計に含まれていないかどうかを簡単に検証できます。また、画期的なフォーマル検証エンジンの性能向上とフォーマルモデルの最適化によって結果品質が改善し、コンピュータリソースの消費を大幅に削減しました。このリリースにはQuesta Formal Multi-Coreも含まれており、フォーマル検証作業を複数のコアやコンピュータに分散できる新しい機能も追加されており、より優れたスループットと演算ファームの消費リソース最適化を実現しています。
「高い検証品質を達成するには、一般的なRTLのコーディングエラーからコーナーケースに潜むバグに至るさまざまな機能上の問題を検討しなければなりません。Questaプラットフォームに追加されたフォーマルベース技術のおかげで、これまでの方法ではうまく対応できなかった問題にも対応できるようになり、検証生産性と設計品質が向上したことに満足しています。」Samsung Electronics、Device Solutions、Master of System LSI Infrastructure Design Center、Byeong E. Min博士は、上記のように述べています。
■設計サイズ無制限の高性能解析用Questa CDC
Questa CDCは半導体業界をリードしている多くの設計チームに採用され、そのキャパシティ、使いやすさ、結果品質が一定の基準値となっています。今回のリリースは、性能が一層向上し、複雑化した今日のSoC（システム・オン・チップ）にも対応できるキャパシティを誇っています。Questa CDCの階層型CDC解析で処理できる設計サイズに制限はありません。ブロックレベルのCDCインタフェースを持つ高精度ロジックモデルを自動的に生成でき、デバッグの完全可視性を備えたチップレベルCDC検証が可能になります。
「人的リソースと技術的リソースの両方で検証全体にかかる時間を短縮するために、高性能で使いやすいフォーマル検証手法を求める声が業界全体で高まっています。Questa検証プラットフォームが提供する新しいフォーマルベース機能は、既存の検証フローにフォーマル検証技術の機能を採り入れることができるため、最先端の性能、高いキャパシティ、自動化という実用性において非常に魅力的です。
メンター・グラフィックス、Design Verification Technology Division、Vice President and General Manager、John Lenyoは、上記のように述べています。
■Questa機能検証プラットフォーム
Questa機能検証プラットフォームは、急増するSoC検証に対応するための独自の包括的なソリューションであり、先進の検証メソドロジ、高性能シミュレーション、インテリジェント・テストベンチ・オートメーション、ソフトウェア／ハードウェア協調デバッグ、フォーマル検証、CDC、ローパワー検証、アナログ／ミックスシグナル、検証IP（VIP）、一元型データベース、自動解析ツール、ESLとエミュレーションとの統合フローにより構成されています。
テスト・スティミュラスを指定せずに設計上のあらゆる機能的な振る舞いを網羅的に解析できるフォーマル検証は、シミュレーション用テストベンチを作成する前の設計サイクルの早期段階での検証を可能にする手法です。しかし、従来のフォーマル検証で謳われていた内容は、熟練したフォーマル解析エンジニアがいる検証チームでなければ実現できず、その達成は大きな労力を要するものでした。Questaは、ボタンを押すだけで誰でも簡単に操作できるパワフルなAutoCheckによる完全自動化されたフォーマルチェックから、より高度なユーザを対象としたアサーションコードのカスタマイズによるプロパティ・チェック機能まで、多岐にわたるアプリケーションを揃えることにより、これまでのフォーマル検証を一変させました。これは、標準的なコンパイル機能やユーザ・インタフェース、UCDB（Unified Coverage Database）にシミュレーション技術およびフォーマル技術をシームレスに融合させた広範な検証ソリューションです。
■Questa CoverCheckによる100%のコードカバレッジ
Questa CoverCheckは、コードのカバレッジ・クロージャを高速化する技術です。カバレッジ・クロージャを達成するには通常、無視できるカバレッジ・ホールかどうかをマニュアルで確認し、無視できないカバレッジ・ホールに対してはシミュレーション用のテストコードを手作業で記述しなければならないため、何週間もの作業が必要です。Questa CoverCheckであれば、専門のエンジニアでなくても、フォーマル手法を活用して、カバレッジ・クロージャを達成できるビンと達成できないビンを自動的に識別できます。その結果、コードカバレッジのサインオフにかかる時間を大幅に短縮でき、スケジュールの見通しを立てやすくなります。また、コードカバレッジのビンが誤って無視されて検証プロセスから漏れてしまうというミスを防止することにより、高い検証品質を確保できます。
■主流ユーザ向けのAutoCheckを搭載したQuesta Formal
AutoCheckは、振る舞いのシーケンスをチェックする強力なフォーマル検証ツールの処理に先立ってRTL設計を解析し、自動的にアサーションを合成します。AutoCheckを使用すると、テストベンチやアサーションをユーザが記述する必要がなく、一般的な機能エラーが設計に含まれていないかどうかを簡単に検証できます。また、画期的なフォーマル検証エンジンの性能向上とフォーマルモデルの最適化によって結果品質が改善し、コンピュータリソースの消費を大幅に削減しました。このリリースにはQuesta Formal Multi-Coreも含まれており、フォーマル検証作業を複数のコアやコンピュータに分散できる新しい機能も追加されており、より優れたスループットと演算ファームの消費リソース最適化を実現しています。
「高い検証品質を達成するには、一般的なRTLのコーディングエラーからコーナーケースに潜むバグに至るさまざまな機能上の問題を検討しなければなりません。Questaプラットフォームに追加されたフォーマルベース技術のおかげで、これまでの方法ではうまく対応できなかった問題にも対応できるようになり、検証生産性と設計品質が向上したことに満足しています。」Samsung Electronics、Device Solutions、Master of System LSI Infrastructure Design Center、Byeong E. Min博士は、上記のように述べています。
■設計サイズ無制限の高性能解析用Questa CDC
Questa CDCは半導体業界をリードしている多くの設計チームに採用され、そのキャパシティ、使いやすさ、結果品質が一定の基準値となっています。今回のリリースは、性能が一層向上し、複雑化した今日のSoC（システム・オン・チップ）にも対応できるキャパシティを誇っています。Questa CDCの階層型CDC解析で処理できる設計サイズに制限はありません。ブロックレベルのCDCインタフェースを持つ高精度ロジックモデルを自動的に生成でき、デバッグの完全可視性を備えたチップレベルCDC検証が可能になります。
「人的リソースと技術的リソースの両方で検証全体にかかる時間を短縮するために、高性能で使いやすいフォーマル検証手法を求める声が業界全体で高まっています。Questa検証プラットフォームが提供する新しいフォーマルベース機能は、既存の検証フローにフォーマル検証技術の機能を採り入れることができるため、最先端の性能、高いキャパシティ、自動化という実用性において非常に魅力的です。
メンター・グラフィックス、Design Verification Technology Division、Vice President and General Manager、John Lenyoは、上記のように述べています。
■Questa機能検証プラットフォーム
Questa機能検証プラットフォームは、急増するSoC検証に対応するための独自の包括的なソリューションであり、先進の検証メソドロジ、高性能シミュレーション、インテリジェント・テストベンチ・オートメーション、ソフトウェア／ハードウェア協調デバッグ、フォーマル検証、CDC、ローパワー検証、アナログ／ミックスシグナル、検証IP（VIP）、一元型データベース、自動解析ツール、ESLとエミュレーションとの統合フローにより構成されています。
