【Verify2013】ルネサス、マイコン開発でのIP組み合わせ検証でフォーマル検証を活用
2013年9月27日、今年で14回目の開催となる検証技術にフォーカスしたセミナー「Verify2013」が新横浜で開催された。同セミナーは検証ソリューションを手掛ける国内外の企業12社がスポンサーとなり開催され、100名近い参加者を集めた。
ここでは、同セミナーで行われた、ルネサス エレクトロニクス株式会社 第一事業本部 グローバル事業戦略統括部 主管技師長 清水 徹氏の講演を紹介する。
※画像の人物がルネサスの清水氏
※画像の人物がルネサスの清水氏
今回、清水氏が講演してくれたのは、社内でのマイコン開発におけるフォーマル検証ツールの活用事例で、使用したツールはOneSpin Solutions社の製品。清水氏によると、ルネサスでは多品種に渡るマイコンの開発を効率化するために、プラットフォーム・ベースの開発手法、すなわち共通化したマイコンのプラット・フォームをベースに、IPブロック化した資産の組み合わせによって派生的に製品を開発する手法を用いており、清水氏はルネサス社内にある日立、三菱、NECと家系の異なる多数のIPを一つのプラットフォームにまとめる仕事を手掛けている。
清水氏によると、プラットフォーム・ベースの開発において大変なのが、様々な周辺IPをプラットフォームに接続した際の組み合わせ検証。ルネサスではマイコン主機能を中心としたPFモジュール、そこに繋がるIPモジュール、モジュールの接続ルール、PF/IPモジュールの機能条件・属性に関するアサーションでプラットフォームを構成しているが、プラットフォームに周辺IPを付け加えた時のバス接続の設定や割り込み制御など、周辺のIPの数や構成に応じて変更が必要になる上、IPをプラットフォームに繋げてシステムが正常動作するかどうを確認するIPモジュールとPFモジュールの並列動作/組み合わせ動作に対する組み合わせ検証がとても重要な課題になっているという。
何が課題かというと、この組み合わせ検証をシミュレーションで行おうとすると、膨大なテストケースとシミュレーション時間が必要となり、カバレッジはテストケースに依存してしまう事になるからだ。また、マイコンの構成が異なるごとにテストケースをチューニングする必要があるため、テストケースを再利用できないというのも検証効率化の上で課題となる。
そこで清水氏はフォーマル検証の活用により、これらの課題を解消した。
プラットフォームの構築で利用しているIPアサーションは、PFモジュールにもIPモジュールにも付いており、IPを接続した時の機能条件が宣言されているため、このIPアサーション間の整合性を証明するフォーマル検証用のアサーションを作成し、機能検証を実施することにした。この手法により、各IPに付属するIPアサーションを再利用できるようになり、検証が完了すればカバレッジも完全となる。フォーマル検証用のアサーションは、各IPアサーションから抽出した条件をマージして作成した。
実際に同手法を用いて割り込み制御の組み合わせ検証を実施したところ、シミュレーションでは547時間要する計算の547通りの組み合わせ検証をフォーマル検証では約73時間で収束することが出来た。テストケースの記述量もシミュレーションでは約13万行という見積りに対し、フォーマル検証ではその10分の1以下で済み検証の大幅な効率化を実現できた。
しかし、清水氏によると同手法では、Glueロジックが入ってくるとアサーションを再利用できないので注意が必要との事で、Glueロジックが制御に影響しない場合はそのままGlueロジックを検証対象に入れてしまえば問題なし。制御信号にもGlueロジックが入ってしまう場合は、Glueロジックとバス制御全てを検証対象に入れ、周辺のアサーションで検証すればそれなりの検証ができるという事だった。
※画像は全て講演資料抜粋のデータ。講演資料は下記URLよりダウンロード可能です。
https://www.eda-express.com/verify2013/seminar.html