いよいよDACに登場、フォーマル検証用の自動バグ検出ツールのVennsa Technologies

DAC2010（6月13日よりアナハイムで開催）に今年初出展する、機能検証ソリューションのVennsa Technologies社。同社のツール「OnPoint」について日本販売窓口を務める木村氏に話を聞いた。

木村氏によるとVennsaは、カナダ・トロント大学の教授Dr. Andreas Veneris氏が2006年に設立したEDAベンチャーで、本拠地はトロント。北米および日本にも拠点を持っている。日本での営業活動は2009年10月から開始しており、既に国内ユーザーを獲得。間もなく日本法人を設立する予定となっている。

Vennsaのソリューションは一言で表すと「バグの原因特定の自動化」を狙ったもので、検証の自動化が進む一方で依然手作業で進められている「バグの原因特定」と「バグの修正」を何とか効率化しようというモチベーションが起点となっている。

現在Vennsaは、「OnPoint」という名のデバッグツールを提供しているが、同ツールのコア・アルゴリズムは20年前から開発されていたもので、近年の「SATアルゴリズム」の進化により大幅な性能向上という恩恵を受け、製品としての販売に弾みをつけた。

「OnPoint」は、フォーマル検証ツールの検出したエラー情報からその原因を自動的に特定してくれるツールで、フォーマル検証ツールとしては市販の名のある製品ほぼ全てに対応。VerilogおよびSystemVerilog、SVA、OVLをサポートしており、ツールに対し対象とするデザイン、エラー情報（期待値と検証結果の差分、反例など）、エラーを再現するためのテストベンチを入力すると、ピンポイントのエラー箇所からコードのバックトレース（自動診断）を行い、コード上の問題箇所を「サスペクト（原因候補）」として出力する。
「サスペクト」は、自動的に概ね30個程度を出力するが、それら候補には「怪しい順に」プライオリティ付けがなされており、木村氏曰く、上位5番位までの候補をチェックする事でほほ100％バグの原因を特定できるとの事。また、「サスペクト」はカテゴライズされており、通常のデザイン上の設計バグだけではなく、アサンプションの欠如、アサーション自体のエラー、システムレベルの接続ミスなどのバグについてもその原因を特定する事が可能。合わせてバグ修正のための情報、ヒントなども提供してくれるという。

木村氏によると、フォーマル検証を提供するEDAベンダ側で「OnPoint」を利用しているケースもあるという事で、検証結果でRTLがおかしいのは分かっていても、その原因が特定できないケースに対して「OnPoint」は非常に有効との事。フォーマル検証ツールを利用するのであれば、「是非OnPointをセットで使い、デバッグ作業の効率化を図って欲しい」との事だった。

尚、「OnPoint」は、現在フォーマル検証ツール向けのソリューションと位置づけられているが、間もなくシミュレーター向けの製品がリリースされる予定だという。

※Vennsa Technologies社