【DAC50】高位合成フローの検証工数を大幅に削減するルネサス流「SLEC」の使い方
6月2日-6日テキサス州オースティンで開催された第50回Design Automation Conferenceの展示会レポート。
Calyptoのブースでは、日本から参加したルネサス・エレクトロニクスの今村 慎太郎氏（第一事業本部 システムインテグレーション事業統括部 ＦＥ設計技術開発部）がユーザーとして、Calyptoの等価性検証ツール「SLEC」の採用事例を発表していた。
今村氏によると、ルネサスが「SLEC」の使い所として考えたのは、高位合成前後の等価性検証で、出来ればRTL検証をしないで済む高位合成フローを構築したいと「SLEC」の利用を試みた。
高位合成前後の等価性検証、すなわち入力するCモデルと高位合成結果のRTLとの機能等価性の検証に「SLEC」を利用するのは比較的ポピュラーな手法で、「SLEC」はCalyptoの高位合成ツール「Catapult」に限らず、Forteの「Cynthesizer」やCadenceの「CtoS」とも連携するパスを持っており、高位合成ツールとセットで「SLEC」を利用しているユーザーは多い。
今回の今村氏の発表で面白かったのは、高位合成前のSystemCコードのプロパティ・チェックを「SLEC」で実施したという例で、ルネサスでは実際のビデオIPの開発において「SLEC」に予め用意されているアサーションを用いて、高位合成用のSystemCコード中の配列外アクセスと未初期化変数のチェックを実施した。その結果、約70の配列外アクセスと10の未初期化変数を検出。同プロパティ・チェックとデバッグに要した工数は約0.5人月で、シミュレーションで実施した場合の見積もり工数約5人月の10分の1の工数で済んだ。これはまさにフォーマル検証の一番シンプルかつ効果の出る使い方であり、当然ながらユーザー独自のアサーションを利用した検証も可能だという。
尚、同ビデオIP開発の約150のモジュール設計全てに「SLEC」を利用し高位合成前後の等価性検証を実施したところ、幾つかのモジュールについてはスタックしてしまい検証出来なかった。そこでルネサスとCalyptoは共同で「Blackboxing Function」および「State-encoding map」という2つの新機能を開発した。「Blackboxing Function」は大きな関数を文字通りブラックボックス化する機能で、「State-encoding map」は、高位合成の合成情報をヒントにステート・マシンの等価性検証を容易化するもので、いずれの機能も網羅検証のキャパシティの問題を解決。これにより全約150モジュールの等価性検証を完了できた。この検証に要した工数は僅か4日間で、RTLシミュレーションの約65分の1の工数で済んだという。
今村氏によると、「SLEC」は高位合成ツールを用いた社内のIP開発フローに標準ツールとして採用したという話で、事例で紹介したビデオIPの開発では、高位合成ツールならびにSLECを用いた設計フローを適用することで、最終的に人手設計の2.4倍の効率化を実現したという事だった。
※記事中のスライド資料は全てルネサス提供のデータ
今村氏の講演の後にCalyptoのマーケティングVPのShawn McCloud氏に話を聞いたところ、同社は業績好調で既にその顧客数は120社以上、中でも「Catapult」の売上強いという事で、2012年には同社の歴史に残るかなり大きな受注を2件獲得したという話。
ツールのアップデートとして今回のDACでは大きなアナウンスは無かったが、「Catapult」はSystemCのサポートやアーキテクチャ・レベルでのローパワー化、インクリメンタル合成、ECO機能など、様々なエンハンスを実施中。この秋口に新たなニュースが出てくるという事だった。ローパワー化ツール「PowerPro」は、RTLパワー解析の速度と精度が高められているほか、パワー記述フォーマット「UPF」もサポートされたとの事、話によると既に「PowerPro」を用いたデザインのテープアウト実績は100件を超えたという。
= EDA EXPRESS 菰田 浩 =
（2013.06.18
）