HECTOR 

次世代のフォーマル・ブロックレベル整合性チェッカ 

概要
次世代のフォーマル検証テクノロジであるHECTORは、テストベンチ、アサーション、カバレッジなしで、独立して開発されたモデル間の高性能なチェックを実行し、継続的で微細な設計変更を網羅的に検証するために構築された、ブロックレベルの整合性チェッカです。

HECTOR
HECTORは、シミュレーションの実行なしでバグの検出とRTLの開発期間の短縮、デザイン変更によるアルゴリズムの整合性の検証を行うことが可能で、ハイレベルのモデルとRTLインプリメンテーション間の変換等価性を検証することによって機能サインオフの確実性が向上します。特許取得済みのコンパイラでワードレベルのRTLおよびフォーマルC/SystemCモデルを生成することにより容量が向上します。また、高性能なフォーマル・アルゴリズムにより証明を数日ではなく、数分または数時間で発見し、独自のリーフレベル・ソルバーで複雑なロジックを解決することができます。HECTORは、証明を早期に収束させるため階層を考慮した等価性、自動デザイン分割、効率的な特許取得済みのメモリー・モデルの利用やマルチプロセッサのサポートを行っています。また、HECTORは Verilog、VHDL、SV、C、C++、SystemC*といった複数の言語をサポートします。

図1
図1. HECTORの概要

HECTORは、ビデオ処理、ワイヤレス・メディア、カメラ、暗号化/復号化ロジック、変換、GPU、浮動小数点などのアルゴリズム集約的なブロックに適し、データパス主体のデザインや、浮動小数点および独自のビットシリアル除算といった数学ブロックを対象にすることもできます。フォーマル空間制御ロジックを含む完全なブロックに対して整合性チェックを実行できるという点もHECTORの特徴です。

*一部のSystemC構造体はサポートされていません。言語のサポート・オプションについてはアプリケーション技術者にお問い合わせください。

図2
図2. HECTORのフロー図

HECTORのデバッグ
バグが検出されると、問題の解決に役立つ反例が提示され、2つのデバッグ・フローがサポートされます。反例をそのままVCDとしてダンプすることも、デザインをコンパイルしてVCS®でシミュレーションしてVPDまたはFSDBにダンプすることもできます。RTLのデバッグにインタラクティブなDVEのフル機能を使用し、複数のデザインを並べてデバッグすることも可能です。HECTORにはC/C++コードに対応するGDBと同様のデバッガ(HDB)もあります。HDBを使用して反例をC/C++コードでデバッグできます。HDBは、DDDなどのグラフィカル・フロントエンドと併用できます。HDBはHECTORのフォーマル・モデルを内部的に処理します。HDBではより強力な制約違反チェックを実行し、未初期化変数へのアクセスに関する警告やコード・アノテーションを得ることができます。

図3
図3. DVEを用いた、HECTORの反例に基づくRTLのデバッグ

図4
図4. HDBを用いた、HECTOR C++の反例に基づくデバッグ

HECTORフォーマル・ブロックレベル整合性チェッカ
HECTORは市販デザインでの有効性が実証されています。HECTORは、テストベンチ、アサーション、カバレッジが不要なブロックレベルの整合性チェッカです。設計期間の短縮、デザイン変更の検証、アルゴリズム仕様に対するインプリメンテーションの等価性検証によりテープアウト条件の達成を支援します。浮動小数点などの数学ブロックでの有効性も実証済みで、ビデオ、オーディオ、データパス、暗号化、復号化、ワイヤレス、カメラ、GPUなどのデザインでも活用されています。詳細については、アカウント・チームにお問い合わせください。



NewsArticlesBlogsSuccess StoriesWhite PapersWebinarsVideosTraining Courses