シミュレーションは性善説的で、フォーマル機能検証は性悪説的だ

かなり前の事だが、ある職場で、 組織の偉い方が、これまでの悪い品質を改善するために「設計段階でバグを混入しない」をその年の目標に掲げ部署全体に説明をしていた 。それはそれで大事なのだが、だからと言って検証の改善をしなくて良いという話にはならないのにと思ったのを覚えている。むしろ、検証のし易さ(再利用の容易性)や精度(観測性とか正確さとか)を高める方が良いのにと思った。

この手の議論は受け取り方が人それぞれで、賛同を得られる場合とそうでない場合が、両方とも極端に偏っている気がする。そして、賛同を得られる場合はCPUやSOC開発などボトムアップの検証スタイルが当たり前の組織に多く、得られない場合は比較的チップトップ検証で全てのバグを潰そうとする組織に多い気がしている。後者の場合、ブロック検証とかユニット検証、単体検証という概念があまりなく、やるとしてもデジタルトップやチップトップで、特定の単体機能を検証するためのシナリオを沢山流し、期待値一致や波形の目視で単体検証をしたことにする組織が多いかもしれない。 機能カバレッジをサインオフクライテリアにすることはできず、やれてもせいぜいコードカバレッジ止まりだったりする。過去に所属した複数の会社の複数部署で両方を見てきた経験から、そう理解している。もちろん、全てがそうだとは言い切れない。

シミュレーションは性善説

「設計で不具合混入を減らすことを最大限に努力するか」または「検証でバグの流出をなくす努力をするか」の議論は、視点を変えて、「設計品質の高いチームと比較的レベルの低いチームが同じ回路を設計した時、最終的に同じ品質を得るために必要な検証プランや検証環境は何か」を考えると分かり易い。 つまり、「設計品質の高いチームの回路はバグの混入の可能性が低いので、機能検証で手抜きできるのか」の議論に帰着できそうだ。ちなみにこの質問に対する私の意見は、「どんなにレベルの高いチームの設計でも 検証の手抜きはできない」だ(注釈1)。

機能検証のゴールは、

の二つで定義できる。上の例では、カバレッジゴールが到達した時に全てのチェッカやアサーションがパスした結果、レベルの高いチームの設計のバグが少ないとか、デバッグのイタレーション期間が短く早くゴールに到達するだけで、二つの開発物の機能品質を高いところで同じにするためには、どちらか一方の検証プランや検証環境で手を抜くことはできない(注釈2)。チーム毎の設計品質が高いか低いかにかかわらず、基本「この回路にはバグがあるはず」という性悪説でやるべきで、バグがないことを想定した性善説では良い検証はできない。

しかし、現実は、検証プランの段階から性善説で行われることがある。特に、シミュレーションでカバレッジゴールを定義する時には、むしろ性善説が必要だ。例えば、ある複数の信号やレジスタ値のクロスカバレッジを見るとき、担当者が関連すると思われる対象のクロスカバレッジ項目を決めるが、無邪気に項目を追加しすぎるとカバレッジ空間が膨大になりすぎてシミュレーションでカバレッジが100%に到達できなくなるので、ある程度項目を狭めるのが一般的な手法である。クロスカバレッジのトランジッション(遷移)カバレッジをとろうとすれば、なおさらである。結果、カバレッジゴールは担当者が妥協に妥協を重ねて十分低く(それでもシミュレーションとしてはそれなりに高い)設定する。実際にはこれらの妥協は多くの場合において正しい判断となるのは、皆さん経験則的におわかりのはず。それは、設計者がバグを仕込ませるような悪意のある設計をしていないことから、絶対大丈夫とは言えないまでも、一般的には正しい判断となる。

次に、設計者が悪意をもってバグを仕込んだ下の回路を見て欲しい。

この回路はイネーブル付きのフリッププロップという単純な回路だが、ある特定の32発の連続シーケンス(11011110101011011011110010101111)が入力された時に50%の確率で不具合が生じるという悪意に満ちた回路だ。こんな悪意のあるバグを仕込んだ場合、シミュレーションでこれを検出することはとても困難である。

不具合発生がある32発のシーケンス入力で50%の確率で起こるとわかっている時、これを真面目に検証するためには、最低でも異なる2^33パターンを入力し、エラーがないことを確認する必要がある。2^33パターンをカバーするためには、例えば1パターンの検証に0.001秒かかったとしてもシングルタスクだと3年近くかかる計算になる。ただ、こんな悪意に満ちた回路を設計することを前提とする必要は一般にないので、こんな努力をする必要はない。

現実に戻ると、いわゆるコーナーケースのバグなどは、設計者に悪意がなくても勘違いなどで偶然仕込まれる。バグはどこに入り込むかわからないので、検証者は、いろいろな組み合わせやタイミング、それらの遷移を駆使して現実的にプロジェクト時間内に完了できるカバレッジ空間を想像しながら検証ゴールを決める。そして、カバレッジゴールが高すぎてゴール達成が無理だとわかれば、設計者や検証者の判断で妥協に妥協を重ねてゴールを下げる。しかし、コーナーケースのバグに対応するためには、やはり性悪説的な考え方が必要になる。結局、性善説と性悪説、この二つの世界のトレードオフで、検証のゴールを決めるしかない。実際、皆さんも、そのようにしているはずだ。

フォーマル検証は性悪説

先ほどの32発の特定のシーケンス入力で誤動作するフリップフロップの検証だが、弊社フォーマル検証ツールのJasperGold を使うと1秒以内にバグが検出できた 。バグを修正した場合に 証明に必要な時間も1秒以内だった。上で説明したように、条件によってはシミュレーションで3年ほどかかる検証が1秒でできる。具体的には、次のようにした。

必要なアサーションは、

assert b |=> c == $past( a )

の1つだけ。「イネーブル信号bが真なら次のサイクルで出力cは1サイクル前の入力aと同じ」という意味になる。当然だが、シミュレーションでもこのアサーションで十分だ。

次に、JasperGold に上の回路を読み込ませ、analyze コマンドを実行した後、elaborate コマンドを実行する。クロックとリセット設定のために、clock clk と reset !rstn を実行する。そして、上のアサーションを環境に追加するために、コンソール上で、assert b |=> c == $past( a ) を実行する(下画像参照。$の前の\はエスケープシーケンス)。

あとは prove コマンドを実行するだけで、とても簡単だ。

上図に示した通り、私の環境では、0.1秒で反例がみつかった。 アサーション “property:0” の横に×が表示されるので、ここをダブルクリックすると、JasperGold の波形ビュアのVisualize が開き、 下のような反例波形を表示される。

回路に仕込んだ32発のシーケンス(11011110101011011011110010101111)がポートaに入力された後に続いて33サイクル目に1が入力されると、次の34サイクル目で出力ポートc が0となるため、アサーションがフェイルする。期待通りの反例波形がすぐに表示される。弊社のJasperGoldは、 与えられたアサーションに違反する入力パターンを独自アルゴリズムで網羅的にかつ効率良く検索しているので、これが可能だ。

もうおわかりの通り、JasperGold を使うと、検証者は入力パターンを作る必要もないし、カバレッジゴールを気にしなくても、このレベルの検証なら、確実にバグを見つけることができる。この例では、32発の特定シーケンスが続いた時に不具合が起こるという事前情報がなくても、アサーションを環境に追加するだけでバグを見つけ、バグ修正後の証明までできた。このヒントがあったとしても、なければなおのこと、シミュレーションではここまで簡単にはいかないはずだ(注釈3)。

最後の妥協

今回のような悪意のあるバグを仕込んだ回路を検証することはなかなかないが、コーナーケースのバグでシミュレーションでは見つけにくく、でも JasperGold だとすぐに見つかる事例は沢山報告されている。

シミュレーションではカバレッジゴールの定義やパターン生成に人間が積極的に介入し、且つ最終的には多くの場合において性善説で検証のカバレッジゴールを下げるが、フォーマル検証ではこのような妥協をせずに性悪説にしたがって、回路内部を全網羅的に検索してバグを探し、検証環境にこそ依存はするがバグがないことの証明までできる。しかも、アサーションや今回は紹介しなかったアサンプションを書くだけで、あとはツールが全て自動で行ってくれる。

とここまでは、回路規模が巨大でなく演算回路が少ないなど 、JasperGold にとってはスィートスポットにはまった理想的な場合の話だ。JasperGold を使った検証で妥協が必要だとすれば、それはアサーションの証明が収束しなかった時だが、この議論はシミュレーションのカバレッジゴールで行う妥協と比較して行わないと誤った解釈をされる場合がある。詳しくは、また別の機会で議論する。


フィールドエンジニアリング&サービス本部
Jasper R&D, Sr Principal Product Engineer
渡口 和信

注釈1:
リソースが不足していて、残りのリソースでどこを検証した方がもっとも効果的かという時に、質の悪い可能性の高い回路により多くの時間やCPU、ライセンスを割いて検証した方が良いという考え方は否定しないが、ここではそのような議論をしていない。


注釈2:
検証でバグが流出してはいけないという仮定の下で議論している。


注釈3:
フォーマル検証もシミュレーションも、適材適所がある。あくまでも、ここで取り上げた例ではフォーマル検証が優れた結果を出す傾向が高いということで、シミュレーション技術を否定するものではない。回路規模の大きなチップレベルや、ゲートレベル検証など様々な場面で、シミュレーションは欠かせない技術だ。

Page Top