フォーマル証明の内側「ヘルパーアサーションってなんだ?」
昨年末の日本ケイデンスのイベントClub Formal 2016において、「ヘルパーアサーションってなんだ?」という声をいただいた。司会者の渡口が思わせぶりに名前だけ紹介して、実体を紹介しなかったためである。
それがなにか、いきなり答えてしまえば、「フォーマル証明の加速を支援するために用意する、実装を説明するためのアサーション」である。アサーションは元来、仕様をフォーマルツールに伝えてデザインを検査するために書くものであった。それに対し、実装の具体的特性を証明エンジンに伝えるための(仕様と直接は関係がない)アサーションが、ヘルパーである。
一つ、具体例を挙げてみよう。リスト1は、FIFOのRTLである。8ワードのFIFOを実現するのに4ビットのポインタを2つ用い、その単純差分で空か満杯かを導出している。このFIFOを利用したデザイン――例えばなんらかのブリッジ――があり、このFIFOを含むアサーション――入口から出口へデータは必ず転送される――があるとする。すると、「wp-rp<=4’d8」という追加のアサーションが先のアサーションの証明を加速する(ことがある)、これがヘルパーである。
先の式「wp-rp<=4’d8」は、この部品中の信号挙動の性質を述べているに過ぎず、デザイン全体とは無関係である。そしてその式をアサーション(証明対象)として宣言する(つまり制約とはしない)のは、実挙動がその式の通りであることもエンジンに証明させたいからである。この式は、証明前は「仮説(あるいは期待、予断、見積もり)」にすぎないが、証明された後は「事実」として利用可能となる。
また別の例を挙げてみる。デザイン中にカウンタが2つあり、一方が他方に、必ず1サイクル遅れて動作しているとする。
このとき、この2信号間には「##1 cnt_b==$past(cnt_a)」という関係がある。であれば、この式はヘルパーアサーションの候補といってよい(挿絵で暗示しているように、両カウンタが別の場所にある場合に。もしcnt_Bがcnt_Aをレジスタ受けしたものであった場合、それは式cnt_b==$past(cnt_a)とまったく同等なので、ヘルプしないだろう。)
さらにもう一つ、少し卑怯な例を挙げる。デザインに検証IP(CadenceのプロトコルABVIP、jasper_~ proof accelerator)を取り付けている時に可能になる技である。検証IPの内実はVerilogのコードとアサーションである。そのVerilogコード内の一部信号挙動と検証対象デザイン内の信号挙動とは、当然ながら、密に関連づくはずである。そこでJasper AEの脳裏には「検証IPが認識しているリクエストの数 == 検証対象デザインが保持しているリクエストの数(これは、ポインタ間の引き算かもしれないし、$countones(validフラグ)かもしれない)」という式が思い浮かぶ。うーん卑怯だ。しかしこれで、デザインとチェッカーとが関連付けられるため、証明が加速しそうな期待がおおいに持てる。
さて、ヘルパーアサーション、おわかりいただけただろうか。この説明で理解いただけた方は、証明の停滞時に、ヘルパーをどんどん書いていただきたい。なお、ヘルパーは、いくつも書いたもののうちで実際に証明加速に貢献してくれたもののことを指す、つまり試行錯誤で見つけるものであることを言い添えておく。さらに、ときにはヘルパーアサーション自体の証明にも時間が必要なことがある(そこでヘルパーのヘルパーを開発する…)。
次回以降は、ヘルパーさんの裏側――どうして証明が加速するか――をご紹介しようと思う。
フィールドエンジニアリング&サービス本部
水野 博之
Latest Issue
- ハイパフォーマンス・コンピューティング分野と車載分野に向けたケイデンスの設計IPソリューション
- 事例紹介:広島大学によるXtensa Vision P6の大腸がん診断支援システムへの適用
- ケイデンスが提供する第3世代論理シミュレータ Xcelium その先進の性能とは?
- デジタル設計効率を大幅に改善する共通ユーザーインターフェースStylus Common User Interface
- 革新的なDRCデバッグを実現 - Results Viewerのご紹介
- もう昔のように作れない。悩める設計者必見!! 先端テクノロジ設計者のためのコンベンション —カスタムIC Advanced Nodeサミット 2017—
- Allegro/OrCAD PCB 17.2-2016 QiR4 PCB Editorアップデートのご紹介
- 編集後記
Archive
2024 Issues
2023 Issues
2022 Issues
2021 Issues
2020 Issues