メンターがフォーマル検証セミナーを開催>>来日した検証の大御所ハリー・フォスター氏に聞く

2007年5月11日、メンター・グラフィックス・ジャパンは、同社品川のセミナールームにて「フォーマル検証セミナー」を開催。業界の有名人である、検証の大御所ハリー・フォスター氏の講演が行われるという事もあり、会場はほぼ満席。70名以上の参加者を集めた。

セミナー関連ページ：http://www.mentorg.co.jp/event/seminar2007/formal/

セミナーは、?メンターの検証プラットフォームの概要説明、?フォーマル検証の利用法と「0-in」ツールの特徴、?「0-in」ツールのデモ、?検証におけるカバレッジ手法、の大きく４つのパートに分かれ、??をハリー・フォスター氏が講演、?はシノプシスの検証セクションからメンターに移ったという、プロダクト・マーケティング・マネージャーのRindert Schutten氏が講演し、?はメンターUS本社のアプリケーション・エンジニア朽木氏が担当した。

ハリー・フォスター氏は、前半の講演「Using Formal Verification to Improve Quality」にて、フォーマル検証の向き不向き、成功の秘訣などを解説。ヒーロー（検証エキスパート）に頼らず組織全体で検証スキルを上げていく事が重要であるとし、特に仕様の文書化から進めていく検証プランニングのステップがキーになると語った。ちなみにハリー・フォスター氏によると、MPEGなど数学的なデータ変換を行うデザインは、フォーマル検証に向かず、メモリコントローラやバス/バスインタフェースなど、データストリーミングレイヤの検証にフォーマル検証が適しているという。

後半のカバレッジ手法に関する講演では、人の力によって創造される・左右されるという反科学的な意味でカバレッジを「ART」と表現。やり方次第で検証効率を大きく改善できるとし、具体的にはラインカバレッジよりも機能カバレッジを重要視するカバレッジ手法を推奨。コードカバレッジが100％でも機能カバレッジが低ければ検証の意味が無く、逆に機能カバレッジが高くてもコードカバレッジが低い（コードを充分に活性化できていない）というケースは、カバレッジの取り方に問題がある。そのような問題を回避するには、仕様をダイレクトにカバレッジにマッピングする手法が有効であると語った。

また、フォスター氏は、カバレッジの話と絡めて、メンターの構築したUCDB（Unified CoverageDatabase）の概要や、自ら活動に参加しているAccellera「UCIS」のカバレッジデータの相互運用に関する標準化活動についても紹介していた。

尚、セミナー終了後にハリー・フォスター氏およびRindert Schutten氏にインタビューを実施。

まず初めに、ハリー・フォスター氏にメンターに移って約１年半の成果を聞いたところ、AVM（Advanced Verification Methodology）のリリースに貢献できた事を上げ、アサーションベース検証に関するノウハウの多くをメンターの検証メソドロジの構築に役立てる事が出来たと回答。Rindert Schutten氏は、ビッグネームであるフォスター氏がメンターに移ったという事自体が大きな成果だと冗談交じりに語った。

次にフォーマル検証の利用方法について、ダイナミックシミュレーションの前と後、どのようなタイミングで使うのが最も効果的なのか？という質問を投げたところ、「それはデザインに応じて使い分けが必要な為、どのような順序が良いかは一概には言えない。」、「肝心なのはフォーマル検証を使うためのプランニングで、シミュレーションで要求を満たすデザインに無理やりフォーマル検証を使う必要は無い」と回答。続いて日本と北米の検証文化の違いについて尋ねたところ、「企業によって多少の差はあるが、さほど大きな違いは無い。」、「日本でも北米と同等にフォーマル検証の利用が進んでいると思う。」とした。

また、メンターのカバレッジデータベース「UCDB」とAccelleraの「UCIS」の活動の関係性について聞いたところ、メンターはハリー・フォスター氏を含め、「UCIS」の標準化活動に積極的に貢献しているとの事で、既に用意している「UCIS」のAPIを標準インタフェースとして提供する事で、業界におけるカバレッジデータの相互運用性を高めていくという形を目指しているとの事であった。

最後に日本の設計者に向けた一言を求めると、「ユーザーコミニュティをより活発化させて様々な設計者の意見をEDAベンダに聞かせて欲しい」と両者は口を揃えて語った。

※メンター・グラフィックス・ジャパン株式会社
http://www.mentorg.co.jp