Siemens EDA/シーメンス EDA

Questa Formal

シミュレーションベースの検証を補間するフォーマル検証エンジン

シミュレーションベースの検証では、テストパターンを追加し、ターゲットとする検証箇所を活性化し、その反応を後段に伝播させて結果を観測します。あくまでもテスト記述の意図に従ってターゲットを活性化し、この生産性を上げる場合にはランダムにテストを振りながら活性化する範囲を広げていきます。これに対してフォーマル検証では、デザイン中のクロックを自動的に進めながら、静的にステート空間を探索し、網羅的に検証します。シミュレーションベースの検証とフォーマル検証を組み合わせることにより、より深く、より広いカバレッジを効率よく達成することができます。Questaではシミュレータとフォーマル検証において共通のコンパイラと共通のカバレッジデータベースが使用できるため、検証フロー全体で品質と生産性の向上を実現します。

シミュレーションベースの検証を補間するフォーマル検証エンジン

フォーマル検証には、アサーションを駆使しながらステート空間を探索しバグの特定やデザインの正当性を証明するプロパティチェックと、特定の検証項目や限られた適用範囲に対して完全に自動化が可能なフォーマルアプリがあります。静的検証ではテストパターンが不要であるため、設計の初期段階から使用することが可能です。またフォーマル向けのアサーションライブラリを使用すると、AXIバスなどの標準的なプロトコルに対する完全遵守を証明することができます。

アサーションベース検証とは

概要

  • テストベンチやテストパターンの準備が整う前の工程から早期に検証を開始
  • 多彩なアプリを使用することで検証項目ごとに完全自動/半自動で検証
  • シミュレータと共通のコンパイラ、デバッガ、多言語対応、カバレッジデータベースが利用可能
  • 性能とメモリ使用効率が高いエンジンはマルチコア・プラットフォームで稼動、高いスケーラビリティを実現

「アサーションベース設計 立ち上げ支援サービス」をご利用ください

Wilson Research Groupが実施した機能検証の市場調査によれば、アサーションを使用する大多数はSystemVerilog Assertions(SVA)を使用しています。SVAは2005年にIEEE標準となっています。新たな手法が登場したときに、それを開発フローに導入するには、言語の習得に始まり、その効果を評価しては改善するなど、多くの労力を要します。
PALTEKではこの労力を低減し、誰もがアサーションを使い始められるようにするための支援策として、「アサーションベース設計 立ち上げ支援サービス」を提供しています。

「アサーションベース設計 立ち上げ支援サービス」についてはこちらをご覧ください

シーメンス EDAのことなら
PALTEKにご相談ください!

シーメンス EDAのことならPALTEKにご相談ください!

シーメンス EDA製品の
お問い合わせ

03-5479-7025

株式会社PALTEK デザインサービス事業部
シーメンス EDA製品サポート窓口