【EDSF 2009】「徐々に馴染めるように」，独OneSpinがフォーマル検証製品の体系を見直し
独OneSpin Solutions GmbHは，RTL検証向けのプロパティ・チェック型フォーマル・ベリファイアの製品体系を見直し，EDS Fair2009（１月22日と23日にパシフィコ横浜で開催）で披露した（ニュース・リリース，同日本語訳）。従来はハイエンド製品が１品種しかなかったが，今回，包含する機能が異なる5品種をそろえた。
今回の製品体系の見直しで，フォーマル検証の習熟度に合わせて段階的に高機能な製品を使えるようにしたという。同社の製品を使ったフォーマル検証手法は他社に比べて緻密で，検証漏れが発生しにくいと見られるが(Tech-On!関連記事)，取っ付きやすいとは言えなかった。
そこで今回，同社は，フォーマル検証を6段階に分けて，それを5製品にアレンジした。フォーマル検証は難易度の低い方から，（1）AutoChecks，（2）Implementation Intent，（3）Functional Requirements，（4）Design Operations，（5）Automatic Gap Detection，（6）Gap-Free Verificationと名付けた。
（1）のAutoChecksは，設計者がRTLを記述した直後に実施する検証を想定している。ツールが内蔵するアサーションとチェッカで処理が進むため，アサーションを記述する必要がない。アレイの制限を越えた処理の発生や，使われないコードの存在，シミュレータ/論理合成に入力できない，といったRTLコードの不具合をチェックできる。AutoChecksの機能を持った製品を「360MV Inspect」とした。
（2）のImplementation Intentは，設計者が簡単なアサーションを書いて行う検証を想定している。アサーションの記述には，「SystemVerilog」が使える。これで例えば，「A信号が発生してB時間後にC信号が発生する」といった内容をチェックできるという。360MV Inspectに「Implementation Intent」の機能を加えた製品が「360 MV Check」である。
（3）のFunctional Requirements以降は，設計者よりも検証エンジニアが担当する検証を想定している。（3）では，Implementation Intentよりも複雑なアサーションを記述して，例えば，AHBやAXIなどの標準プロトコルに対する準拠や，アービトレーション・ストラテジの正当性などをチェックする。なおOneSpinによれば，（1）から（3）は，他社のフォーマル・ベリファイアでも実行可能だという。
（4）のDesign Operations以降は，OneSpinの製品でしか実行できない機能になる。（4）ではRTL記述に含まれる「動作」を抽出する。ここでは主にOneSpinの検証手法を習熟することが目的で，検証自体は（6）で行う。360 MV Checkに（3）と（4）の機能を加えた製品が「360 MV Verify」である。
（5）のAutomatic Gap Detectionでは，検証されていない入力シナリオを抽出する。（4）と同じく，（6）の準備段階とも言える。360 MV VerifyにAutomatic Gap Detectionの機能を加えた製品が「360 MV Assure」となる。
そして（6）のGap-Free Verificationが，同社が推すフォーマル検証手法になる。（5)までで準備したデータを用いて，漏れのない検証を実行する。全機能を備えた製品が「360 MV Certify」で，これが同社が従来から販売していた製品である。
さらにOneSpinは今回，360 MV Verify以上に付属するデガバ・ソフトウェアを更改した。RTLデータ（構造情報）の表示，入力値の時間推移の表示，波形の表示が可能。また，問題が発生した場合，その原因となった個所をRTLデータ中で特定することができるという。「ピン・ポイントで原因個所を特定できるのは，われわれの製品だけ」（OneSpin）。
