Club Formal Japan2016レポート

2016年12月8日に、Club Formal Japan2016を開催いたしました。今回は、これまでとは違ったフォーラムにしよう!ということで、USで行われているJUG(Jasper User Group conference)のように、参加者の皆様とも活発に意見交換ができる場にすることができたら、我々にとっても面白い上に勉強にもなるし、お越し下さる皆様にも有意義な時間にして頂けるのではないか?と、関係者一同で企画をいたしました。登録受付開始からすぐに定員オーバーとなり、キャンセル待ちまでして頂くことになった際には、喜びとともに、ご期待に応えなくては!のプレッシャーもとてもありました。私の持ち時間としては、JUGの様子をお伝えする5分間だけだったのですが。。。

企画の初期段階で話に挙がった”JUG“ですが、恥ずかしながら、存在そのものも知らなかった私にとって、想像はしてみるものの、そんなに面白いものなのか?他のユーザーミーティングと一体何が違うのだ?と、謎ばかり膨らんでいたところ、視察のチャンスが訪れたのはClub Formal開催1ヶ月前。半信半疑で本社USへ。 
JUGで得てきたことや、感じたことは山のようにあったのですが、Club Formalに参加頂きました皆様に、あの5分間で雰囲気だけでもお伝えできていたのであれば光栄です。

画像をクリックすると拡大表示されます

JUGは11/2-11/3の2日に渡って開催され、Key Noteを含めた14のご講演を頂きました。詳細は、cadence.comのHomeページから、各プレゼンテーションをご覧頂けますので、是非、参考にして頂ければと思います。どのご講演もとても素晴らしかったのですが、私のお奨めプレゼンは、1日目の「Jasper Practical Application」です。

CDNLiveとの大きな違いは、当たり前ですがJasperGoldだけにフォーカスされているという点です。そのためフォーマル検証に関わっている方々の熱気に包まれながら、朝早くから丸々2日間たっぷりとフォーマル機能検証についての事例やお話を伺うことができました。お昼休みには、JasperGoldの各アプリを使ったデモコーナーもテーマ毎に用意されており、ツールの動作を直接見て頂きながらQ&Aに対応している現地スタッフは、どのテーマも多くのお客様に囲まれており、まるで日本の通勤ラッシュ時のような人だかりの中、スクリーンに食入るようにデモを見て下さっている姿も印象的で、それぞれのアプリへの関心度の高さを目の当たりにしました。ユーザー事例のご講演では、スピーカーの方々の目を輝かせた熱い語りはもちろんのこと、Q&Aの際に交わされる言葉や会場の雰囲気から伝わってくる皆様の熱意にも圧倒されました。この雰囲気を日本でも出せるのだろうかという不安と期待で迎えた2016年のClub Formal。ご参加いただきました皆様には、JUGに参加されていたお客様に勝る勢いで積極的に議論にもご参加頂き、大盛況のうちに終了いたしました。ありがとうございました。
2017年は、さらに面白いものを目指して準備いたしますので、皆様も是非舞台の上で講演されてみませんか?事例発表のエントリーもお待ち致しております。

Club Formal2016では、いくつかアンケートを実施させて頂きました。ご協力下さいました皆様、ありがとうございました。集計結果をご報告いたします。

●シールでお答え頂きましたアンケートの結果
Q.フォーマル検証に対するネガティブな意見をお持ちであればお聞かせ下さい。

図1:インピーダンスチェック

  1. 収束しないからダメ。収束すべき・・・(37票)
  2. シミュレーションが必須のため、フォーマルが追加タスクになる ・・・(38票)
  3. 擬似エラーが多い・・・(30票)
  4. 波形を見ないと安心出来ない・・・(37票)
  5. 証明出来ても信用できない・・・(11票)
  6. その他/いずれでもない・・・(33票)

赤いシールは4つずつお渡しし、1番~5番までの項目に複数回答可能で貼って頂きました。1つの項目に複数貼られていたお客様もいらしたようです。6番の「その他/いずれでもない」には、どれにも当てはまらない場合に1つシールをお貼り頂いています。ネガティブなイメージを払拭できていないのは、我々が十分にご説明できていないことの反省点としても受け止めました。皆様の不満や不安を解消していけますように、活動をしていきたいと思います。たとえば2番の“シミュレーションが必須のため、フォーマルが追加タスクになる”ですが、新たにプロパティを書き、不慣れなツールを起動するのは”追加タスク”にも思われるかもしれません。ただここで、手法によらずテストベクトルの総量が同じと仮定するなら、フォーマルがベクトル作りを代替してくれる分、シミュレーションの労力が軽減されます。同時に、バグの早期発見や、検出率向上、トータルの検証時間を短縮することができたとの報告をいくつも頂いております。もしまだJasperGoldをお使い頂いたことがないようでしたら、是非一度お試し頂きたいと思います。効果がありそうなブロックや階層をご検討頂き、短時間でシミュレーションと同じか、それ以上の検証品質が達成できることを見ていただければ、追加のタスクがあっても、やる意味があることを実感頂けると思います。

   

“擬似エラーが多い”につきましては、会場でも沢山ご意見を頂きましたように、その原因を解析することで、仕様書の不備や不足や、プロパティ記述のミスなどを見つけることができます。これらを修正することで検証環境の品質向上や、仕様の勘違いなどの早期発見につながります。また、JasperGoldでは、波形表示もVisualizeを使って簡単に行えます。もし上記ネガティブなイメージによって、フォーマル検証の実運用をためらわれておられるようでしたら、是非ご相談下さい。

Q.使用されているアサーション証明を収束しやすくするための技術をお聞かせ下さい。

図1:インピーダンスチェック


青いシールは、4つのシールをA~EのそれぞれYesかNoかのどちらか、又は”その他“に1つだけ貼って頂きました。既に色々と工夫して使われていらっしゃる方が多くいらっしゃるのだなという印象でした。Nondeterminismにつきましては、アンケートでもご要望がありましたので、ご紹介の機会を設けたいと思っております。

記述によってご回答いただきましたアンケート結果です。5点満点でご評価頂きました満足度も、ご発表頂きました皆様のお陰であることはもちろんですが、ご発言頂きました皆様のお陰もあって、平均4.46と高い評価を頂きました。 コメント欄にも、「お客様発表やそのQAがとても参考になった」「全体的に大変満足だった」というご意見を沢山頂き、関係者一同とても喜んでおります。

●御社のフォーマル検証の適用状況についてお聞かせ下さい図5.Import機能

Club Formalに参加して下さった皆様の96%の方々が、フォーマル検証について考えていらっしゃることがわかりました。既に適用頂いている皆様には、是非フォーマルを活用して良かった点、苦労された点、工夫されている点などを次回のClub Formalで共有して頂けると幸いです。またご検討中の皆様や、お困りの点などのある方々は、是非ご連絡下さい。ステージに上がりましたAEと共に、良い方法をご提案させて頂きます。

●フォーマル検証適用において障壁となる要因についてお聞かせ下さい(各項目で1つ選択)

フォーマル検証適用において、“大きな要因”と多くの方にご回答いただいたのは、知識と経験という結果でした。JasperGoldを使って、楽しくフォーマル検証の経験をどんどん増やしていって頂けたらと思います。また、フォーマルカバレッジ指標や、ROIの見せ方につきましても、JG-COVでフォーマルカバレッジ検証品質観測、vManager でシミュレーションカバレッジとのコンバイン技術で進捗観測、Expert Systemで運用状況からROIの観測など、様々な方法がございます。お客様がお困りに感じている導入障壁を壊すお手伝いをさせて頂けると幸いです。

さて、「議論1:フォーマル機能検証は収束しないからダメ?」の冒頭で、アイスブレークとして出題しました以下の問題を覚えていらっしゃいますでしょうか? 回答が気になられている方のために、ご紹介します。

問1の答えは2枚です。具体的には、奇数の「1」と漢字の「漢」をめくるだけで、良品チェックは十分です。

理由は、奇数の「1」の裏がもし漢字であればそれは不良品なので、「1」の裏は漢字ではないことを確認する必要があります。「漢」の裏をめくる必要があることは、自明なので説明は省略します。また、「22」は偶数ですが、その裏はどんな文字がきても問題ないので、めくる必要がありません。「ア」はカタカナですので、その裏はどんな数字でも問題ありません。今回、文字の裏は数字(数字の裏は文字)であることが前提条件なので、これを確認するためにすべてをめくる必要もありません。

いかがでしたでしょうか? 私は、「22」をめくる必要がない理由を納得するまでに時間がかかってしまいました。今年もご期待に応えていけます様、知識を増やし、技術を磨いていきたいと思います。JasperGold共々よろしくお願い致します。


フィールドエンジニアリング&サービス本部
志賀 玲子

Page Top