 |
|||||
 |
|||||
 |
|||||
|
|||||
|
1. はじめに SystemC Japanオフィシャル･サイトでは、形式検証に対して理解を深めてもらうために、定期的に内容を追加し、連載のイメージで掲載していきます。このページは、山本修作（カリプト社）が担当することになりました。まだ形式検証を扱っている会社は当社だけですので、自然と私がその執筆をする事になりました。形式検証に興味がある方が多く、期待は大きいぞという天の声に舞い上がってしまいました。日々の業務で取り扱っている形式検証のツールを中心にハードウェア向けの等価性検証について情報を発信してゆきたいと思います。 とは言っても形式検証のエンジン内部の解説は期待しないでください。高校･大学の数学では水面すれすれ飛行の常習犯であった私にその適性があるとは思えません。必要に迫られたら、英語論文を直訳して人々を路頭に迷わすか、別の人に後始末をお願いして敵前逃亡すること必至です。よって今後の内容は、道具として「使う」「応用していく」ことを主眼においた展開を考えています。 プロパティ･チェッキングに関しては、初稿時点ではSystemC対応の市販EDAツールがありません。執筆適任者が現れるまで、あとあと後ろ指を指されない程度に述べたいと思います。私は、ツールにプロパティを食わせることを結構好んでするタイプですので、少しの期待くらいなら大丈夫です。 いずれにしても、これまであまり知られていないSystemCの形式検証の世界へようこそ!! 多くの人々を禁断の世界へ導くことをミッションとし、その洗脳活動に邁進(?)したいと意気込みだけは持っています。しかし、もともと筆不精ですので、もし更新が滞るようなことがあれば、応援のemailでお知らせいただければ幸いです。一般的にこれを催促と言うらしいのですが。 最後に、これを読まれる方への助言です。くれぐれもうまい話には騙されないようにしてください。世の中おいしい話はそうそう転がってはいませんから。まあ、あくまでも一般論としてです。 2. 形式検証 形式検証とは、設計対象物を計算機工学における数学を基盤とした技術を用いて仕様記述やプロパティと照らしあわせ、その設計対象物が仕様に対して正しく実装されていることを証明する、あるいは正しくないことを証明することを言います。 これは、インターネットに上にあるいくつかの定義をつなぎ合わせて書いたものです。しかしRTLの形式検証技術として、すでに等価性検証(LEC; Logic Equivalence Checking)とプロパティ･チェッキング(Property Checking)がよく知られていますので、難しい定義から入るよりもこれを基点に話を進めることにしましょう。 等価性検証は、二つでのデザイン間の機能的な等価性を検証します。プロパティ･チェッキングは、仕様もしくは期待動作を専用言語もしくはHDLで記述し、設計対象物がそれを満たしているかを検証します。どちらの検証技術もテストベンチの作成やシミュレーションは不要であり、数学的な証明技術によって検証シナリオ内での高い網羅率を誇ります。 3. SystemCの形式検証 私の主観ですが、SystemCでの形式検証が従来のVerilogやVHDLによるRTLと比べて大きく異なる点が二つあります。その一つはSystemCそのもの、つまり取り扱う言語の違いであり、二つ目は抽象的な時間の概念です。 SystemCを取り扱うということは、取りも直さずC++言語の持っているオブジェクト指向の取り扱いを意味するはずです。SystemVerilogにもオブジェクト指向の能力が備わっていますが、検証環境の構築に使われることはあったとしても、設計対象に使われそうな流れはこれまで聞いたことがありません。特に合成(形式検証)サブセットに関して言えば、従来のものに少し手を加えただけです。 SystemCの場合、その用途として主流と言えるTLMは言うに及ばず、ハイレベル合成(HLS: High Level Synthesis)を考えてみた場合でも、そのような制約の強いサブセットをSystemC形式検証が受け入れることはできません。 オブジェクト指向とプログラミング言語C/C++との親和性こそがSystemCの最大の特徴であり、抽象化、高い再利用性をもたらす普及の根源であるからであり、当然ながら形式検証ツールもこの特徴を最大限に引き出せる必要があるのです。 時間の概念を従来のRTL形式検証の視点から見た場合、クロック･サイクルが基本単位となっています。ここでもSystemCの用途を考えた場合、Untimed、TLM、更にはHLSへの入力からRTL出力までを考慮する必要が出てきます。つまり、これらの異なる時間の概念を何らかの形で一貫して取り扱う必要性が出てきます。 特に等価性検証の場合は、異なる抽象度(時間の概念)を持つ二つのデザインを比較しなければならない場合があり、この問題は非常に重要です。プロパティ･チェッキングにおいても、設計の詳細化に伴って、上流で作成した抽象的なプロパティを後工程で再利用する場面があれば、その際にも異なる時間の概念の取り扱いが問題になるかもしれません。 4. SystemCの等価性検証 SystemCの等価性検証では、どのような使い方が考えられるでしょうか。ここでは代表的なものとして次のようなものをあげてみました。左辺がreferenceで右辺が検証対象とします。 (1) SystemC HLS model 対 合成後のRTL (1) SystemC HLS model 対 合成後のRTL (2) Algorithmic C 対 SystemC HLS model (3) SystemC HLS modelのリファインメント (4) 既存のRTL対SystemC HLS model (5) 既存のRTL対SystemC HLS model (1)から(3)までは、トップ･ダウンでの等価性検証であり、(4)と(5)はボトム･アップでの等価性検証であると言えます。形式検証のツールは、このうち(1)から(4)までにいずれにも適応することができます。(5)に関しては、残念ながらSystemC TLMの書き方がSLECのSystemC サブセットの範囲を超えているために、この執筆時点では適応できません。
|
|||||
 |
|||||
 |
|||||
