ブロックからチップまで、フォーマル技術を使用した厳密なカバレッジドリブン検証
OneSpinは、IPおよびブロックレベルから完全なシステムオンチップ(SoC)までのRTL検証、およびFPGAデバイスのインプリメンテーション検証に対する総合的なフォーマルベースソリューションを提供しています。このソリューションは5つの主要な検証タスクにフォーカスしています:
- 早期の、自動化されたコード検証により、迅速に設計を反復し敏捷な設計を行う
- 独自のモデルベースのミューテーションカバレッジによる包括的なアサーションベースの検証
- 自動化されたアプリを使ったスケーラブルなインテグレーション検証および機能解析
- 高度な最適化を行ったFPGAインプリメンテーションの検証
- 高位合成前にSystemC/C++コードに対して機能検証を行い、簡単にバグを検出
敏捷なハードウェア設計
IC設計プロセスにおいてバグを早期に解消することは時間と労力の節約になります。そのためコンポーネント設計者にはより多くの検証を行わねばならないプレッシャーがかかっています。しかし従来のシミュレーションベースの検証テクニックでは、結果的に設計者がスティミュラスの作成や検証全般への関与により多くの時間を割くことになり、クリエイティブな設計に費やす時間は短くなってしまいます。
OneSpinのDV-Inspect™ 設計評価ソリューションは、テストスティミュラスを記述する必要のない閉ループの敏捷なハードウェア設計反復を可能にし、検証に関わる負荷を設計者から取り除きます。アジャイル開発では、設計者が小規模で価値の高いコードセクションを作成し、素早くテストし、統合していくインタラクティブなモデルが求められます。こうしたアイデアはICハードウェア設計にも広く当てはめることができますが、検証テクニックの点から見ると、そこには新たな考え方が必要となります。
OneSpinはセットアップと使い方のオーバーヘッドが低い検証ソリューションを提供しています。そこではスティミュラス作成のない設計作業が実現され、何ページもの偽陽性結果に手間取ることなく本当の問題を自動的に追跡し、ボタンを押すだけでコードの最適化をチェックすることができます。
フォーマル技術を使って、OneSpinのDV-Inspectは次を提供します:
- 設計の動作をスティミュラスやグラフィカル操作またはシナリオの設定をほとんどまたはまったく使わずに観測する機能。これにより設計者はコード内で何が起こっているかをすばやくまた手間なく確認することができます。 必要であれば後のシミュレーション用としてテスト作成も自動化することができます。
- 静的な検査機能によりさまざまな問題をフォーマルレベルでチェックできます。単にコードの構文をチェックするのではなく、コードの処理を調べて本当の問題を見つけます。これによりログファイル分析にかかる何時間もの作業が節約できると同時に、より難しいバグを検知することが可能になります。
- 正しいプロトコルの使い方を徹底し、リセット後のXステートを解消するなどの各種自動化アプリにより、時間のかかかる各種作業を簡素化することができます。
アサーションベース検証
ICのすべてのブロックを徹底して完全にテストすることはきわめて重要です。単純なバグであっても量産ICに含まれれば修正のコストは大きく、フィールドで壊滅的な製品故障を引き起こすこともあります。ブロックレベル検証は従来複雑なテストベンチを使用し、多数のバッチモードでのシミュレーション実行が必要でした。それを可能にする検証能力があっても、検証クロージャの達成は、特にシミュレーションコードカバレッジ指標に基づいた場合、困難なことが多いと言えます。
フォーマル検証では、アサーションを使用して記述された機能プロパティが実証または反証され、この方法で最も複雑な設計シナリオも完全に検査することができます。様々なシナリオを妥当な時間内に検証し、テスト対象ブロックを完全に含めるには、優れたフォーマル技術が必要です。OneSpinの360 DV-Verify™ は高度に最適化されたフォーマルモデルを構築し幅広いフォーマルアルゴリズムを駆使して設計を可能な限り迅速かつ効率的に検証します。さらに、このソリューションには高度なデバッグおよび使いやすさのための機能も含まれており、問題の追跡とデバッグが簡単に行えます。
閉ループのメトリックドリブン検証ソリューションを実現したOneSpinのQuantify™ は、精密なモデルベースのミューテーションカバレッジを提供します。このテクノロジは設計のコードを解析することによりいかなる変化も少なくとも1個のアサーションをトリガすることを確認し、全体的なカバレッジ指標を提供するとともに特定のカバレッジの穴を見つけるのにも役立ちます。
統合検証
IPをより大きなブロックやサブシステムに統合することは、常に多大な検証リソースを必要とします。これらのデバイスには階層バスやネットワーク構造、精密な電源制御やクロッキングスキーム、さらにはセキュリティ機能などが含まれているのが普通で、検証は複雑かつ多面的なものになります。フォーマルテクニックはこのレベルにおいて効果的に適用することができ、必要なインテグレーション解析および機能解析の大部分を提供し、多くの検証タスクを自動化することができます。
OneSpinのブロック統合検証ソリューションはフォーマル技術に基づいた、開発フローのさまざまなフェーズに有効で特に統合のタスクに効果的な、さまざまな自動化アプリを活用しています。ブロックのフレームワークは、設計プロセスの最初に作成され、設計者がコンポーネントを組み込み、検証チームがテストとアサーションを構築して毎晩リグレッション解析を行う、というケースもあります。または、プロセッササブシステムも含めたSoC全体が設計プロセスのもっと後の方で統合されることもあります。
どちらにしても、IPとブロックを統合するにはモジュールの組み合わせのインテグレーションチェックと機能性チェックの両方が必要となります。これらのチェックは従来シミュレーションによって行われてきましたが、これらのサブシステムの規模を考えると、シミュレーション実行を設定してこれらを徹底的にテストすることは難しくなりました。OneSpinのフォーマルアプリはこの時間のかかるエラーの起こりやすいタスクの負荷を大幅に軽減します。多数の標準的なインテグレーション要件、たとえば主要な信号の接続関係、レジスタのアドレッシングならびに動作、そして標準通信プロトコルの使用などを、自動的にチェックすることが可能です。
OneSpinでは、インテグレーションに関する作業に特に効果的であり、また設計の他のフェーズでも有効な、各種自動化アプリを提供しています。これらを使ってシミュレーション/エミュレーションの負荷を削減することができます:
- Structural Analysis: 的を絞ったフォーマルベースの構造コード解析
- Safety Checks: 標準的なコーディング問題のオペレーショナルチェック
- Activation Checks: コードセグメントがアクティベート可能であることをチェック
- Score Boarding: 機能的通信チャネルの整合性
- Protocol Compliance: バスプロトコルのインプリメンテーションを確認
- Register Checks: レジスタをIP-XACTアドレスマップと比較
- Connectivity Checking: デバイス構造内の主要な接続関係をチェック
- X-Propagation Checking: 電源投入と不定の可能性チェック
インテグレーションに関係したその他のタスクを解決するためのアプリもパートナー企業から入手可能です。これらのアプリはOneSpinフォーマルプラットフォームとサードパーティ製品との統合を可能にするOneSpin 360 LaunchPad™機能を使って、各ドメインのエキスパートにより開発されたものです:
- Specification Validation: 高度なシステムレジスタ仕様バリデーション
FPGAインプリメンテーション検証
FPGAは静的なハードウェアマトリックスを使用し、レジスタとレジスタ間ロジックの割合がほぼ決まっています。また、最高品質の設計を実現するため、アグレッシブな最適化を行う最先端の自動化された設計フローが使用されています。これらの最適化の組み合わせを様々なRTLコードに適用すると、「システマティック」エラーの発生につながることがあります。これらのエラーは予期せぬ形で発生し、検知には時間がかかり、潜在的に破壊的影響を持っています。
OneSpinのEC-FPGA™はこれらの問題を、FPGA合成結果に対してフォーマル検証を適用することで防止します。これにより設計の動作に最高の信頼性を実現するとともに、開発スケジュールや結果品質(QoR)の改善にもつながります。これはFPGAに対して膨大なリグレッションテストを行うよりも格段に優れた方法です。こうしたテストにおいてはスティミュラスの作成と実行に何日もかかるのに加え、RTLとゲートの等価性も保証されません。
さらに、問題が特定された場合でも、FPGAデバイス内のデバッグ可視性が限定的なため、問題の根本原因を特定することは困難です。また、問題を解決した後にもプロセスを再度やり直す必要があり、時間のかかる再合成と、以前と同じく膨大なリグレッションテストを行わなければなりません大規模なFPGAデバイスの場合、またはセーフティクリティカルなアプリケーション向けの場合、これは設計スケジュールに対して許容できない負担となる可能性があります。
EC-FPGAはRTLネットリストをRTLソースに照らして検証します。EC-FPGAはリタイミングされたFPGAデザインを扱える独自の機能を備え、合成および配置配線(P&R)フローにおいて発生するシステマティックエラーを突き止めるのに効果的なツールです。これらの高度な最適化はステートエレメントを変化させることも多いため、EC-FPGAはシーケンシャル等価性チェックによりRTLとネットリストのマッピングを行います。このソリューションは大手FPGAベンダーにも採用され、自社の合成ツールのテストや主要なFPGA合成フローのサポートに利用されています。
OneSpinのEC-FPGAを使用することにより次のような利点があります:
- すべてのシステマティックな問題が排除されたことを確認でき、テストとデバッグが加速される
- 複雑なテスト作成やシステマティックエラーを予測する必要性の解消
- 最終的なデザインにコーナーケースバグが存在しない確証による信頼性の向上
- 最もアグレッシブな最適化を適用でき、消費電力、速度、使用率が向上
C/C++検証
高位合成(HLS)はアルゴリズミックな、アンタイムドのこともある、多くの場合SystemCやC++で記述された設計モデルを完全にタイムドのRTL設計ブロックに変換します。HLSツールはマイクロアーキテクチャを変更した設計コンポーネントを短時間に生成するとともに、アルゴリズム処理データパスを高速かつ効果的に最適化する方法として特に人気があります。これは柔軟性と市場投入までの期間の点で大きなメリットを生みます。その結果、HLSは現在多くの大手半導体および電子システム メーカーで使用されています。しかしながら、SystemCとC++設計に対する検証オプションは合成技術の進化についていっていません。
SystemCツールの選択肢が限られていることから、検証タスクの多くは合成後のRTLコードに対して行われており、間接的な段階が加わることでSystemC/C++レベルでの問題解決は複雑かつ時間のかかるものになります。さらに、SystemC規格においては、不定またはXステートの欠如や、スレッド間の競合状態の可能性により、さらなるあいまいさが生じ、これらを合成前に排除しなければなりません。この抽象的な設計レベルに関連した問題は、適切な検証手法を使用すれば簡単に解決でき、最終的な設計品質の向上につなげることができます。
OneSpinのSystemC/C++設計検証ソリューションは、フォーマル検証環境を提供することにより高位合成前にSystemC/C++コードに対して機能検証を行い簡単にバグを検出します。様々なタイミング レベルや抽象度のSystemCおよびC++コンポーネントに幅広いフォーマル検証テクニックを適用することが可能になります。
初期化されていない値の伝播や、未定義のオペレーション(配列範囲外など)の影響などのハードウェアの問題は、OneSpinの自動化されたアプリを使ってSystemC/C++レベルで効果的に検知することができます。DV-Verify™にはSystemC専用の自動化された算術オーバーフローチェックが追加されており、算術データパスの数値制度を検査することができます。
アサーションベースの完全なフォーマル検証もサポートされており、包括的な、時間的SystemVerilogアサーションあるいはCアサートをSystemC/C++コードに対してテストすることができます。これにより、合成後のHDLコードにも適用できる一般的なアサーションメカニズムを使った豊富な検証機能が提供されています。
More information…
OneSpin 360 DV-Inspect™ takes designer’s pain away and automatically and exhaustively analysis RTL source code prior to functional verification and synthesis, eliminating hard to find implementation errors early in the design process.
»Learn more about DV-Inspect™…OneSpin 360 DV-Verify™ goes beyond that by providing a unified, coverage-driven assertion-based verification flow, and including a full verification app library, as well as means for easy design exploration, all in one tool.
»Learn more about 360 DV-Verify™…OneSpin 360 EC-RTL is an easy to use Sequential Equivalency Checking tool that to ensures functional equivalence between RTL design revisions.
»Learn more about 360 EC-RTL…360 EC-FPGA is an automatic sequential equivalence checking tool that provides a fast and efficient method to ensure that aggressive synthesis optimizations have not introduced systematic errors that could disrupt the final design.
»Learn more about 360 EC-FPGA…OneSpin provides a complete set of formal apps as part of OneSpin 360 DV. On top of that, additional innovative capabilities are available, targeting for example safety critical design, or hardware security as special apps and from third party providers.
»Learn more about our DV Apps Library…OneSpin 360 DV-Verify™ goes beyond that by providing a unified, coverage-driven assertion-based verification flow, and including a full verification app library, as well as means for easy design exploration, all in one tool.
»Learn more about the Quantify Coverage App…The OneSpin 360 Design Verification (DV) product line leverages the most advanced, high-performance formal technology as the basis for a range of verification solutions, from automated design analysis to advanced property checking.
»Download the flyer…The OneSpin 360 EC-FPGA solution ensures that advanced FPGA synthesis optimizations, used to achieve competitive functionality, performance, power consumption, and cost targets, do not introduce functional errors.
»Download the flyer…OneSpin 360 DV-Verify extends the DV- Inspect platform with coverage-driven Assertion-Based Verification (ABV). Many entry-level formal apps allow for assertion generation for specific problems without a need for deep formal knowledge.
»Download the data sheet…360 DV-Inspect automatically inspects the RTL code once it has been compiled, without the need for any testbench setup.
»Download the data sheet…The OneSpin 360 EC-FPGA™ solution ensures that advanced FPGA synthesis optimizations, used to achieve competitive functionality, performance, power consumption, and cost targets, do not introduce synthesis and optimization errors.
»Download the data sheet…OneSpin® 360 EC-FPGATM is an automatic sequential equivalence checker that prevents field programmable gate array (FPGA) design flows from introducing synthesis, place-and-route and other implementation errors.
»Download the data sheet…This white paper presents an implementation signoff flow proving that the final FPGA netlist is functionally equivalent to the RTL model. Based on FPGA-specific, mature formal verification technology, the solution is exhaustive and efficient, catching many issues before synthesis starts.
»Download the white paper…"We had a positive experience in adopting formal verification within a RTL development process that implemented Agile-recommended practices in a localized, low-risk fashion. This approach appears to be an effective and pragmatic way to improve the RTL development process by harnessing some of the benefits of Agile." Sergio Marchese, Verification consultant at TeraStatic.
»Read the full article on Tech Design Forum…"The incremental approach allows for feedback between teams far, far sooner than would typically happen using a waterfall approach. The feedback exchanged between teams that are working toward the same goals simultaneously gives many more opportunities to clarify design intent and holds far less potential for long schedule slips." Neil Johnson, Principal Consultant – XtremeEDA Corp., Bryan Morris, VP Engineering – XtremeEDA Corp.
»Read the full article on AgileSoc.com…"Agile development techniques are now sweeping through the software community transforming the way we develop software. But apart from a few isolated reports the hardware community has been largely untouched by this revolution." François Cerisier and Mike Bartley, Test and Verification Solutions.
»Read the full article on Design & Reuse…"While there are obvious differences between software development and hardware development, there are also significant similarities. The key for hardware developers is to resist getting caught up with the differences and to instead focus on the similarities. Doing so makes it hard to argue that the values of the agile manifesto and agile practices could not be used to achieve the same benefits that software developers have been realizing for years." Neil Johnson, Principal Consultant at XtremeEDA Corp.
»Read the full article on EE Times…We are uncovering better ways of developing software by doing it and helping others do it. Through this work we have come to value:
»Read the complete Agile Manifesto…Muhammad Haque Khan, product specialist for Synthesis Verification, is speaking about our FPGA-specific, mature formal verification technology, that is exhaustive and efficient, catching many issues before synthesis starts.
»Watch the video now…Get in touch!
Learn more about achieving functional correctness with OneSpin!
Sven Beyer, Product Manager Design Verification