フォーマル証明の内側「ヘルパーアサーションってなんだ?」
第2回
前回は、ヘルパーアサーションとはなにかを紹介した。以下4条件を満たすもの、である。
1. 証明したいが時間切れする(あるいはより素早く証明したい)ターゲットプロパティに対し
2. そのロジックコーン内の信号挙動を記述し(主に実装に言及していて、ターゲットプロパティと意味上の連携がない)
3. ターゲットプロパティより容易に証明でき
4. ターゲットプロパティの証明を高速化する、アサーション
1~3に該当しながら4に該当しないものも存在するが、それらはヘルパーの候補が落選したということである。ときどき「ヘルパーアサーションの書き方を教えて」と頼まれることがあるのだが、そこに万能な技はなく、書いては試しまた書いては試す、ということを繰り返さなくてはならない。
ヘルパーがなぜヘルプするか、まずはマクロな仕組み(あるいは原理)を述べよう。それは、人間が知っている、あるいは気付いた回路の具体的特性を、ヘルパーアサーションによって、証明エンジンに「予備知識」として授けることができるのである。元来DUTを動作させながら“知る”はずであったことがらを証明エンジンが事前に“聴き知る”ことができるため、証明を速やかに終えられるのである。お終い。(お忙しい方は、次の仕組み編を読み飛ばしていただいて結構です。)
では、以下でミクロな話をしよう。証明エンジンが一体ロジックをどう“考えて”いるのかを体当たり的にお伝えしたい。前回のFIFOのコードを素材としよう。彼(?)は「FIFOである」と自称しているので、検証エンジニアは「それが本当にFIFOであるか」を確かめる必要がある。FIFO検証は多くの場合、スコアボードという検証部品を取り付けて「全ての出力データは、入力された通りである」を確認すればよい。Jasperが提供するスコアボードjasper_scoreboard_3を取り付け証明を実行すると、たちまちdata_integrityアサーションが証明される。ここでは証明エンジンにはTriを選んだ。
さてお立会い。元のコードに「初期化時にbody[7:0] <= 0;」という記述を追加することができる。このデータレジスタのゼロクリアが、実用的に不要であること、そして不要ながらも動作に支障はないことの2点は、直感的には自明であろう。だが検証たるものそれではいけない、念のため、新コードでも証明を実行してみよう。
あ、あれ、悩み出しちゃった。10分以上も考え中? Jasper調子悪くなっちゃった? Cadenceさん、壊れてますよー… ちなみにこの後、1037秒でようやく証明が終了した。元の3秒とは大違いである。エンジンが検討したサイクル(Bound欄)も、先の17に対しこちらは32であった。この違い、人間にとってはとても不自然であろうが(3年前にこれを「発見」した当時の僕もおおいに驚いたことを告白しておく)、決して壊れているのではなく、フォーマル証明の特性なのである。社内課金が気にならない方はぜひ一度お試しあれ。
フォーマル証明のエンジンは、当然ではあるが、人間がするようにはデザインを認識していない。ではどうしているかというと、超並列シミュレーションを行いながら、FFがどの値を取ったかを記録し続けているのである。プロパティのロジックコーンに対し、許されているすべての入力を与えながら超並列シミュレーションを行っているうちに、コーン内のFFがどの値を取り得るか(そして取り得ないか)をいつか完全に知ることができ、取り得る値すべてにおいてプロパティ式を評価することでアサーションに違反がないことが確定する(→証明できた)のである。コーン内にFFが計nビット存在するとき、その単純連結Vの最大2n通りの値について、それが実現可能か不能かを確かめているのである。(実際には種々のエレガントな手法が用いられている)
ここで一部のFFが初期化されていないとき、調査は格段に楽になる。初期化のないFFに対し証明エンジンは初期値として0/1のいずれをも付与することができるので、初期化ありの場合に比べ、見たい状況を素早く作り出せるのである。例えば下図の状態を“作り出す”のに、元のコードではサイクルを必要としないが、初期化ありコードでは17サイクルが必要となる(dinからbodyへ、64’h1、64’h2、…を実際にpushしなくてはならない)。この不自由さが、証明の所要時間と検討サイクルの増加をもたらしているのである。
さて、長らくお待たせしました、ヘルパーアサーションである。内部ネットの挙動がプロパティ式として取り出せていて証明済みなのは、エンジンの証明過程においてどういう意味を持つだろうか。ヘルパーの式は真と判明しているのでターゲットの証明中も常に成立するべきで、ということは、ターゲットを支配しているVにおいて、ヘルパー式を偽にするような値はその不存在を「即座に断言」することができる。一部の値の不存在を、思い悩まず探索を行わずして簡単に知り得るがゆえに総計算量を減らすことができるというのが、ヘルパーがヘルプしてくれる理由の、乱暴かつ定性的な説明である。
なお、候補がヘルパーになり損ねる(証明を高速化しない)こともあると本稿の最初に断った。この理由は、その候補アサーションが主張している事象に、エンジンが容易に(ことさら知識を授けられずとも)「気付いて」しまうからである。(実際のヘルパー開発でも繰り返し書いては試すので、次第に、エンジンの機嫌を取っているような気分になってくる。)
理屈の次は実験に移ろう ―― が、今回の単純なFIFO検証環境では、事前知識「wp - rp≦8」は証明を助けることができなかった。仕方がない、スコアボードをjasper_scoreboard_2に差し替えて違いを観察してみることにする。なんだかまるで尻尾が犬を振るような話であるが、ご勘弁。スコアボードという検証部品の内部にもいろいろあるのだなとご理解いただければと思う。検証コードと、スクリプトと、結果を示す。鼻薬程度には効いているという結果であるが(82秒→68秒)、エンジンを差し替えると効果絶大であった(エンジンC、6600秒→260秒(再び尻尾が犬を振るような…))。
最後に実オペレーションについてご紹介して本稿を終えることとする。ヘルパー開発時には、Jasperを2つ起動する(または1つを起動した上で「セッション」2つを使用する)とよい。まず両方に同じ検証環境(デザインと、難しいターゲットアサーション)をロードしておく。ヘルパーアサーション候補を思いついたとき、両方にそれを追加登録する。一方ではその候補自身の証明を起動し、思いつきの正しさを確かめる。他方ではその候補を「証明済み」とマーク(assert -mark_proven)した上でターゲットプロパティの証明を起動し、証明進捗が速まるかを確かめる(ProofGrid Managerで、折れ線の傾きが急峻になる等)。両方が満たされた時、そのアサーションは晴れてヘルパーに登用させられる。
フィールドエンジニアリング&サービス本部
システム&ベリフィケーション
シニアAEマネージャー
水野 博之
この記事に関する問い合せ先:
コーポレート・マーケティング部
E-mail:cdsj_info@cadence.com
Archive
2023 Issues
2022 Issues
2021 Issues
2020 Issues