ニュース

360 MVの自動化された証明ベースのSystemVerilogアサーション デバッガ


OneSpin 360 MVの証明ベースのアサーション デバッガはSystemVerilogアサーション(SVA)が失敗する箇所と時間を自動的に特定します。 他のフォーマル検証ツールでは手間のかかるマニュアル作業となるデバッグ工程を大幅に短縮することにより、360 MVは機能要件と動作の検証に使用される複雑なアサーションの開発を簡単に、短期間で行えるようにします。

アサーションの証明が失敗すると、デバッガはアサーションに違反する動作を示す反例の形で診断情報を生成します。 この反例は360 MV環境でデバッグすることも、SpringSoftのVerdi™ Debug Systemまたはその他のVCD(Value Change Dump)波形ビューアにエクスポートすることもできます。

機能

360 MVデバッグ環境はストラクチャルSVAデバッガ(図の左側)、マルチビュー対応のデザインビューア(図の右側、テンポラル ファンインビューを表示)、波形ビューア(右下)で構成されています。 これらの組み合わせにより高速かつ高精度なデバッグに不可欠な高いレベルの観測性が得られます。

360 MV Debugger

OneSpinの360 MVアサーションデバッガは高速なデバッグに不可欠な自動化と観測性を提供します。

  • ストラクチャル デバッガには失敗したSVAアサーションの簡単な例が示されています。 アサーションの結果は6個の条件で構成されています。 デバッガは失敗した条件をハイライトし、DUVにより満足された条件はハイライトされていません。 ユーザーはアサーションのサブエクスプレッションを展開することにより複数の階層レベルにわたりSVAを調べることができます。 ユーザーはハイライトされたパスをたどるだけで、エラーとなったサブエクスプレッションを特定できます。
  • デザインビューアは階層、ソース、テンポラル ファンインおよびファンアウトを含む複数のビューを持っています。
  • テンポラル ファンインビューでは設計階層内でのある信号の他の信号への依存関係を表示します。 ユーザーは簡単にマウスクリックで信号のファンインを展開し、その信号に影響するあらゆる値をトレースすることができます。
  • 3つのメインウィンドウにはそれぞれ状況依存メニューがあり、アサーション定義に対してソースコードエディタを開く、信号の宣言にジャンプするなどの操作を素早く行うことができます。
  • ユーザーは各ビュー間でアイテムをドラッグ&ドロップし、迅速に設計を確認できます。 たとえば、テンポラル ファンインビューにある信号を波形ビューアにドラッグすることにより、その時間的動作を反例全体に照らして分析することができます。
  • デバッガは選択されたタイムポイントにおける信号値のアノテーションを、ストラクチャルデバッガおよび/またはテンポラル ファンインビューなど複数のビューでダイナミックに表示します。