Cベース設計とは？　導入の課題は？　――人手による介入が必須，完全自動合成は幻想

●フォーマル・ベリフィケーションが重要に

　そうすると今度は，人手の介入があるということで，各設計段階における検証技術が重要になります．例えば，図5に示すアーキテクチャに対して，図7に示す設計手法が考えられます．

　まず，プログラム的に記述されたC言語から出発します．ハードウェア化すべき部分は関数の再帰的呼び出しやポインタ操作などを使用しないものに書き換えます．また，システムLSI内で並列実行すべきところは，そのような記述に変換していきます．こうして，最終的にハードウェア部はRTL記述に，ソフトウェア部はC言語記述（OSなどの機能を利用した並行動作を含む）に変換されます．

　この設計手法では，「設計済みの記述をライブラリ化する」，「そのためのテンプレートを作成しておく」などを行うことによりIPマクロの再利用も行え，システムLSIの有効な設計手法の一つであると考えられます．このような設計手法（設計の流れ）においては，各設計変換（合成を含む）における「等価性検証」と，各設計段階における「プロパティ検証（いわゆるモデル・チェッキング）」が重要です^注．大規模なシステムLSIを対象とすると，それなりに規模の大きい回路の検証が可能である必要があり，やはり研究段階であるには違いないのですが，検証問題としては通常よりも楽になる場合があります．

　つまり，図7に示す設計の流れの場合，特に等価性検証において，等価であるか否かをチェックする二つのC言語の記述がかなり近い（両者の記述の大部分が同じ）ことが期待できます．すると，RTLや回路レベルの等価性検証と同種の技術を使って，大規模設計の等価性検証を行える可能性があります．実は同様のことがプロパティ検証についても言えます．図7の設計の流れを仮定すると，けっこううまく検証できる可能性があります．

 注；等価性検証やプロパティ検証は，設計データを数学的に解析して論理機能を検証するという意味で，「フォーマル・ベリフィケーション（形式的検証）」と呼ばれている．等価性検証は，二つの設計データの論理機能が等価であるかどうかを調べる．プロパティ検証は，設計された論理回路が特定の設計仕様（プロパティ）を満足しているかどうかを調べる．

〔図7〕C言語に基づくハードウェア・ソフトウェア協調設計の流れと検証支援
図5に示すハードウェア・ソフトウェア協調設計を支援し，また，図6に示すRTLの各設計段階を支援するうえでは，上位レベルと下位レベルのC言語記述の等価性検証と，各設計段階のプロパティ検証が重要となる．特に，等価性検証は，時間のかかるシミュレーション作業を省くためにも，形式的手法による完全な検証が望まれる．