フォーマル機能検証は収束しないからダメ?

はじめまして

2016年5月に入社しました渡口(とぐち)と申します。よろしくお願い致します。

私は今回の転職をするまで、国内外の大手の半導体設計会社を経験しました。SOC(System On Chip)やビデオコーデックIP、イメージセンサなど多種多様のチップ設計と検証に携わってきました。会社が変われば当然設計や検証文化は異なりますが、同じ社内でも組織が変わると、前の組織の常識が、次の組織では非常識だった経験もしました。ECO(Engineering Change Order)1件で怒鳴られる職場から、10件でもいいからスケジュールに間に合えば良いという職場もありました。バグを沢山みつけて感謝されることが多いですが、「設計のレベルが疑われるから」と煙たがられることもありました。現場においては正解は必ずしも一つでもないことを、現場を通して経験してきました。これら経験のすべてが、私の財産だと思っています。

JasperGoldとの本格的な出会いは、国内メーカーに勤務していた2008年です。その面白さからすぐに虜になり検証実績を積み重ね、同社での最後の1年半はフォーマル機能検証技術を社内で広める業務を任されておりました。その後、外資メーカーに転職しました。もともと興味があったEDA業界で100%フォーマル検証にうちこめるチャンスがあることを知り、ツールを使う側から売る側への転職を決めました。

現在、JasperGold のPE(Product Engineer)という立場で、国内はもとより海外のお客様や海外で活躍するPEやAE(Application Engineer)たちと仕事をしています。見えてくるのは、海外のお客様が大量にJasperGoldを購入し、積極的に弊社AEやPEからサポートを受け、様々なリクエスト出している現状、その結果ツールの成長とともにユーザー様もすごいスピードで拡大し成長する様子です。私も17年近くお世話になった上述の国内メーカーで、レベルの高いフォーマル検証チームの一人として仕事をしていた自負もありますが、アジアをはじめ世界のお客様からいただく質問やリクエストのレベルの高さを見せつけられて、「これはすごい」と思わず口から出てしまうほど。日本も負けてはいられません。「日本のフォーマル検証技術はレベルが高いから、日本の設計検証は品質と効率ともに抜群に高い」が世界のあたりまえになるように、日本の半導体業界に少しでも貢献できれば幸いです。

フォーマル機能検証は収束(注釈1)しないからダメ?

記事のタイトルにこれを選びましたが、それにはいくつか理由があります。

覚えていらっしゃる方もおいでと思いますが、昨年2015年11月に新横浜で開催されたDSForum (Design Solution Forum)2015では、2時間枠で「フォーマル検証トーク」と題して、フォーマル機能検証のパネルディスカッションが行われました。私も当時はJasperGoldユーザーとして参加させていただいたのですが、その時に感じたのは、「皆さんフォーマル検証に対して、まだ否定的な意見をもっている」でした。例えば、こういう具合です。

いろいろ出ました。私(このリンクの左上の写真のスクリーン下、客席先頭列に座るメガネをかけた坊主頭)は客席で手を上げて質問とコメントをさせていただきました。だいたいこういう内容でした。

ネガティブな意見が多くきかれますが、誤検出のエラーを見つけても、アサンプションを追加修正しながら機能仕様の確認が早期にできるメリットはなかったですか?その過程でコーナーケースのバグは見つかりませんでしたか?同じバグを見つけるためにシミュレーションではとても困難だった経験はありませんか?パネリストの皆さんのご意見をお聞かせください。


結局プログラムの進行上、私の質問をパネリストの皆様に聞いて頂くことは実現しませんでした。同様の意見は、昔所属した職場や社内でコンサルティングをした部署でも、たくさん聞かされてきましたので(もちろん部署によって異なりますが)、これが日本の半導体設計検証の割と標準的な状況なのかなと、私としては確認できた、そういうフォーラムだったと記憶しております。

そして5月に今の会社に入りました。世界の検証現場からの情報が毎日24時間、メールボックスに飛び込んできます。この業界に入らないと分かり得ない国内のお客様の情報もいろいろ見えてきました。これを書いている時点で、約4ヶ月間EDA業界にいて、現時点での私個人の結論は、

「日本の検証技術はまだまだ伸ばせる!」

です。海外ではツールができることはツールに任せるのが少しだけ我々よりも上手なのかもしれません。現場で伸びしろがあるからこそ、本格的にメソドロジやツール、検証言語を学んで環境に実装してしまえば、海外企業はきっと日本企業についてこられません。是非、我々に、皆様の技術スキルをのばし、国際競争力を高めるお手伝いさせてください。

フォーマル機能検証とシミュレーションの比較

そのきっかけ作りにもなるClubFormal が、今年も12月に予定されております。お客様の検証事例発表はもとより、皆様と検証技術やメソドロジを議論する時間を設ける予定です。例えば、「フォーマル機能検証は証明が収束しない、扱いが難しい」というご意見を持つお客様にも会場にお越しいただいて、他の会社にお勤めになるエンジニアの皆様と、この日ばかりは会社の枠を取り外し議論する、そんな楽しいセッションを計画しております。我々からは、収束させるためのテクニックはもちろん、収束しなくてもたくさんのメリットが有ることを議論を通して紹介させていただきます。例えば、下に紹介する内容も議題の候補の一つです。以下では、フォーマル機能検証とシミュレーション(フォーマル機能検証ではない動的検証)を比較することで、証明問題を別角度から見ていきます。

検証エキスパートの皆様は、シミュレーション向けに機能カバレッジでクロスやトランジッションなどを駆使し、合理的に妥協しながらも抜け漏れのないカバレッジゴールを設定されているはずです。ランダム検証の自動化でカバレッジを埋めに行きますが、埋まらなかったカバレッジホールはレビューで安全と判断されればクライテリアから除外します。リリース直前になればなるほど、膨大さを増したレビュー作業は形式的となり、連日終電ギリギリまで行われるレビューの品質は下がるかもしれません。アサーションやチェッカを書かず一部目視で検証を終わらせているために、バグ修正後のリグレッションで、正しい検証ができていないかもしれません。慣れ親しんだシミュレーションでは、「時間がないから」「仕方がないから」と、その検証フローにどこか寛容になりがちです。または「どこか妥協するしかない」、と言うべきかもれませんが。

しかし、未知のフォーマル機能検証になると、とたんに「絶対収束するべき」と高級で完璧なゴールを求め、少しの妥協も許せない方もいます。「収束しないことがあるから使えない」と結論づけてはいませんか?もし、そうだとしたら、それは非常にもったいないです。

なぜでしょう?

なぜなら、実際は一般に収束するアサーションの方が抜群に多いからです。また、収束問題に直面するとしてもその前に、シミュレーションでは発見が困難なバグが比較的早期に見つけられることもメリットの一つです。さらにもう一つ言うと、シミュレーションでは絶対に必要な、入力信号をドライブする環境(ドライバやバスファンクションモデル、シナリオ、ランダム制約等)がフォーマル機能検証では不要なため、環境構築に必要な工数が劇的に削減できるのもよく知られたメリットです。だめ押しの一発は、カバレッジゴールを埋めるために、シミュレーションを何度も走らせる、カバレッジを観測してホールを見つけてそれを埋めに行く、いわゆるシミュレーションでやられるカバレッジドリブン検証がいらなくなります。つまり、待っていればそれが埋まりだし、収束すれば100%カバレッジが埋まったと判断できます。証明が収束した後、「本当に100%カバレッジが埋まったといえるのか?本当に不足はないのか?」の議論は、下で紹介するClubFormal 2016の別の議題にとても相応しいと思います。

ClubFormal2016のご紹介

改めてご紹介いたしますが、今年も12月にClubFormalを開催いたします。国内の優れた検証技術者が集い議論を楽しみ、フォーマル機能検証技術の優れた点やJasperGold を使うメリットなど、さまざまなヒントが見つかる技術フォーラムになる予定です。他社様どうしで成功体験をシャアすることは、一見敵に塩を送るようにも見えますが、むしろコンペチタは海外に多くいると考えるならば、国内は「チーム日本」で、是非お客様同士でメソドロジを共有しレベルアップをして頂きたいなと、個人的に思っております。そして皆様が職場に戻られた際には、それぞれの現場に最適なJasperGoldの活用に繋げられる、そんな技術フォーラムになると大成功です。

「フォーマル機能検証は収束しないからダメ?」

一年越しで昨年のDSForumの「フォーマル検証トーク」の続きの議論を、皆様と一緒にできることを楽しみにしております。

最後になりますが、証明が収束しなかった場合の対策もちゃんとご用意しております。バウンデッドプルーフ(Bounded proof)の概念はJasperGoldが業界でいち早く導入したメトリクスです。証明のための抽象化技法などをGUI上で教えてくれるJGES(JasperGold Expert System)という新しいアプリもあります。当日、時間が許すかぎりご紹介していきます。

 

過去のClubFormalへのリンク: 2013/2014/2015

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

注釈1: フォーマル機能検証では、RTLとアサンプション制約で一意に決まる到達可能な空間内に、アサーションで書かれたルールに違反する状態が無いかを検索エンジンを用いて検索します。同空間を全網羅的に探索したのち、反例が見つからなかった場合、証明作業が収束したとなります。一般に、回路規模が大きくなると、収束までにかかる時間が長くなります。

Page Top