ルネサスエレ、マイコン・プラットフォームの検証で独OneSpinのフォーマル検証を採用

2011年5月16日、フォーマル検証ツールを手掛ける独OneSpin Solutionは、ルネサス エレクトロニクスが同社のフォーマル検証ツール「OneSpin 360MV」を採用した事を発表した。

発表によるとルネサス エレクトロニクスは、MCUプラットフォーム向けの機能検証環境を構築するにあたり、OneSpinのフォーマル検証ツール「360MV」と合わせて提供される「オペレーショナルABV」と呼ばれるライブラリを採用した。

「オペレーショナルABV」は、タイミング・ダイアグラム全体を単一のアサーションで記述するためのSVAライブラリで、ルネサス エレクトロニクスでは同ライブラリとフォーマル検証ツール「360MV」を組み合わせて利用する事で、プラットフォーム開発における製品展開時の動作確認を素早く実施したいというニーズを満たした。

実際に「360MV」をベースに構築された検証環境は、MCUプラットフォームの動作確認において論理シミュレーションベースの検証環境よりも50倍高速であることが実証されており、MCUプラットフォームを構成する各機能ブロック間の接続確認（バストランザクションなど）をチップレベルで従来手法よりも短期間に実施することが可能になったという。

OneSpinによると、「オペレーショナルABV」を利用する事でアサーションの開発をよりシンプルに効率化する事が可能で、わずか1日のトレーニングを受けるだけで、エンジニアはタイミング・ダイアグラム全体のアサーションを直感的かつ簡潔に記述することができるようになるという事だ。

※OneSpin Solution社