Design Solution Forum 2017 実行委員の酒井です。セミナー当日は多くの皆さまにご来場いただき、誠にありがとうございました。この記事では、私が担当した企画「フォーマル検証ディスカッション」で行われた議論の内容を紹介します。
本企画は、「フォーマル検証」というひとつの技術にフォーカスして、ベンダとユーザを一堂に集めて言いたいことを言い合おう、という意図で開催したものです。そんな趣旨の下、事前に募集した議題の中で最も参加者の関心の高かった「フォーマルサインオフ」の話題から、議論は始まりました。
当日の議題一覧。吹き出し内は参加者の興味の分布
しかし、ふたを開けてみると、議論は「検証とはどうあるべきか」という一般的な話題に広がっていく、予想外の展開となりました。その中で浮き彫りになったのは、設計・検証を高度化していく上での課題は技術論だけでは語れない、ということ。エンジニアの教育体制やベンダとの協力関係の構築など、適正なインフラが整って初めて、新しい技術が活きてくる、ということでした。議論がどのように展開していったのか、順を追って振り返っていきます。
- フォーマル検証の充分性は、どうやって保証する？
- レビューしやすいテストプランニングの基本ルール
- 実装と同じことをプロパティで書かないためには？
- フォーマル検証で避けて通れない収束性問題、議論は思いもよらぬ展開に
- 収束性の議論から見えた、日本と海外の考え方のギャップ
- 間違った方向に導かないためのフォーマル検証エンジニアの育成方法
- フォーマル適用に必要な多くの要素は、ダイナミック検証でも必要
- フォーマル／ダイナミック切り分けの判断基準
- 感想、謝辞
先に書いた通り、最初の議題として取り上げたのは、フォーマル検証のサインオフ基準の話でした。ダイナミック検証と比較するとノウハウの蓄積が不足していることもあり、ユーザ同士でもお互いにどのような考え方でサインオフしているのか、気にされている様子でした。
議論ではまず、フォーマル検証ツールが持つ検証充分性指標の測定機能が示されました。例えば、各アサーションを証明するために必要なコードの範囲を計算して重ね合わせていくことで、検証に使われたコードのカバレッジを導き出すことができます。このような指標を用いることで、コードに対する検証の完全性を客観的に証明できます。
このように、ツールは検証完了の判断の手助けをしてくれる一方、判断そのものをツールに委ねることはできません。最終的な判断は人間がしなければならないというのは、どんな検証手法にも共通する事実です。そこで考えなければならないのは、ツールが出してくる指標はあくまでコードベースであるということです。検証項目が（実装されたコードではなく）仕様書に対して充分であるか、合致しているかをレビューすることは人間しかできないので、人間はそこに注力すべき、という議論になりました。そこで重要になってくるのは、いかにレビューしやすい検証項目を策定するか、という点でした。
テストパターンを人間が考える必要のないフォーマル検証では、検証項目の策定はプロパティの策定と同義です。プロパティと仕様の紐づけが明確に行われていることが、正しいサインオフ判断を行う上で最も基本的かつ重要なことと言えます。これを前提としたうえで、実装したプロパティの妥当性（アサーションに抜けがないこと、過制約になっていないこと）を確認するためにツール機能を活用する方法が、ベンダの方々より提案されました。
また、プロパティのわかりやすさもレビューのしやすさに大きく影響する、ということも、議論の中で共有できた意見でした。前提条件が細かすぎるなど、テストパターンをそのままプロパティ化したような記述はレビューを難しくするため、フォーマルのプロパティはできるだけ抽象度を高くした方が好ましい、という意見の他、プロパティ化が困難な仕様はプロパティ検証ではなく等価検証の適用を検討すべき、という提案もありました。
抽象度の低いプロパティとして典型的なものに「RTL実装と同じことを書いてしまう」というものがあります。この問題については、全ての検証は第三者検証であるべき、という指摘がありました。設計者が検証者を兼ねる場合でも、自分が設計した部分は他の人に検証させる、ということを最低限のルールとすべきでしょう。ただし、反例の解析は設計者の介在が重要になることが多く、デバッグは検証と分けて考えるのが適切と言えます。
フォーマル検証で避けて通れない収束性問題、議論は思いもよらぬ展開に
続いて、議論はフォーマル検証の収束性の話へと移りました。テストプランからサインオフまできれいな筋道が描けたとしても、検証が収束しなければ、そこでまたつまずくことになります。収束しない検証対象には、どのように対処していけばよいのでしょうか？議論ではまず、「ある程度のbound数（網羅的に探索したサイクルの深さ）でよしとする」か「何が何でも収束させる」かという、2つの方向性が示されました。
ある程度でよしとする場合、合理的な妥協点を探る必要があります。どこまで探索できれば検証できていると言えるのか、その判断材料には、ツールの持つbounded解析（指定したbound数で到達可能なコード範囲を特定）機能が活用できそうです。しかしここでも、最終的な判断は人間に委ねられるしかない、という結論になりました。
一方、何が何でも収束させる、という場合、ユーザが検討する必要があるのは収束させるための工夫です。例えば、収束しないアサーションの証明を助けるようなアサーションプロパティ（ヘルパーアサーション）を追加していく、という方法があります。ヘルパーアサーションは収束しないアサーションのPass/Failには影響を与えないので、検証項目としてのプロパティの記述作法に囚われず書くことができます。設計者の力を借りて、実装に近いアサーションを書くことで手間を削減する、という手法も取り得ます。
収束性を向上する上で最も簡単なのは、利用する計算資源を増やすことです。あるベンダの方の実感では、人間の工夫が必要なのはアサーション全体の2～3割で、残りの7～8割はCPUの並列利用数を増やすことで収束する、とのことでした。そして、欧米のユーザの並列利用数は、日本のユーザに比べて圧倒的に多い、という事実が示されました。単に「収束しない」と言っても、日本と欧米ではその悩みのレベルに大きな開きがあるのかもしれません。
並列実行のためには潤沢な計算資源とツールライセンスを確保しなければならないため、少なくない額の投資が必要です。日本のユーザが投資拡大に踏み切れていない理由については――議論は日本企業の意思決定プロセスの問題にまで進展して大いに盛り上がったのですが、とかく目下の課題としては――熟練したエンジニアが不足していることと、必要性が浸透していないことが挙げられました。まだまだ日本の検証フローは人海戦術で何とかしている部分が否定できず、フォーマルに限らず新しい検証技術に適応するためのエンジニア教育が必要という点は、意見の一致が見られました。もちろん教育をするためにも初期投資は必要ですが、そこは新技術を導入しないのもリスクと捉えて、将来を見据えて考えていくべきでしょう。
また、フォーマル検証特有の問題として、検証エンジンが中でどう動いているのか見えにくいために収束性の対策が取りづらい、という意見がありました。これに関してはユーザ側で何とかできる問題ではなく、ベンダによる解析作業が必要不可欠ですが、ここでもコラボレーションの考え方に対する日本企業と欧米企業の差が見えてきました。秘密主義で知られる米国の某有名企業ですら、EDAベンダの解析に対しては協力的なのだそうです。日本企業の場合、一概に悪いとは言えないものの、設計データの社外への開示には総じて慎重な姿勢であるようです。情報の守秘と開示のポリシーについても、合理化する余地があるように感じました。
間違った方向に導かないためのフォーマル検証エンジニアの育成方法
フォーマルサインオフの議論では、サインオフの判断のしやすさはプロパティのわかりやすさに左右されることがわかりました。翻ると、複雑なプロパティは検証完了の誤った判断を招き、不具合の流出にもつながります。このような失敗がフォーマル検証に対する不信感を植え付け、ツールへの投資を抑制させる一因にもなっている、という声もありました。
このような残念なボタンの掛け違いを防止するためには、エンジニアの育成方法を考える必要があります。ここでは、「フォーマル検証の考え方を正しく理解することこそが、危険な使い方をさせないために最初に学ぶべきことである」という見解にたどり着きました。機能検証にフォーマルを導入するとなると、どうしてもプロパティの実装方法や収束性を上げるテクニックに目が行きがちですが、まずは根底にある考え方を共有できているか、立ち止まって確認する必要があるように思いました。
海外に目を向けてみると、欧米ではフォーマル検証専任のエンジニアを置いていることが多いようです。プロパティ品質や収束性はエンジニアの経験度合いに依存する部分も大きいため、問題の発生したプロジェクトに即座にエキスパートを配置できるような体制も必要かもしれません。
フォーマル適用に必要な多くの要素は、ダイナミック検証でも必要
検証完了判断にフォーマル検証特有の考え方が必要な一方で、検証フローそのものはダイナミック検証と大差ない、という見方もあります。明らかに異なるのはテストパターンを入力しないことくらいで、アサーションまたはそれに類するチェッカは、現代的な検証フローでは普遍的に使われているものです。
この観点からは、ダイナミック検証でも「現代的な」フローを取っていない職場、例えば波形の目視チェックに未だに依存しているような職場では、フォーマル検証のハードルは当然高くなる、という指摘がありました。プロパティを定義するための明確な仕様書と、そこから正しくプロパティを書き起こす検証スキルは、現代の検証では採用する手法に関わらず必要なもの、と捉えるべきでしょう。
回路規模が大きい場合、通常は全てをフォーマルで検証することはせず、検証項目ごとにフォーマル検証適用可否の切り分けを行うことになります。フォーマル検証とダイナミック検証のエンジニアが充分に育った組織では、次の課題はここになるでしょう。続く議論では、この切り分けの判断をマニュアル化できないかという問題提起がありましたが、判断の基準には経験則による部分も多く、明確な結論には至りませんでした。
また、例えば、フォーマル検証が苦手と言われる演算処理系の回路でも、プロパティ検証ではなく等価検証であれば効果的に用いることができます。したがって、フォーマルとダイナミックの二項対立ではなく、より幅広い視野で最適な手法を検討するべき、という意見がありました。
議論のレポートは以上です。参加されていない皆様にも、会場の熱気が少しでも伝われば幸いです。最初にも書いたように、「フォーマル検証ディスカッション」と銘打ったものの、その領域にとどまらない幅広い課題が色々と見えてきた気がします。国内外の他のユーザがどのようにフォーマル検証を活用しているのか、生の声を聴く機会は私に取っても貴重でした。
議論を盛り上げていただいた参加者の皆様には、この場をお借りして感謝申し上げます。特に、自社ツールのプロモーションの範囲を超えて忌憚ない発言をいただいたメンター山本様、シノプシス野々下様、ケイデンス渡口様、リアルインテント神田様、ワンスピン齋藤様、大変お世話になりました。このような場に対する経験の不足により、至らない点やお聞き苦しい点も多々あったかと思います。来年に向けて、よりご満足いただける企画を練っていきたいと思っていますので、これからもどうぞよろしくお願いいたします。
文：Design Solution Forum 2017 実行委員 酒井 皓太