インタビュー：フォーマル検証サービスの英Axiomise

2025年8月20日、論理設計の機能検証にフォーカスしたカンファレンス「DVCon Japan」が品川で開催された。

DVCon Japan 公式ページ

今回、DVCon Japan 2025に出展するためにイギリスから来日したAxiomise社のCEO、Ashish Darbari氏にインタビューを実施した。Axiomise社はフォーマル検証による検証サービスやコンサルティングを手掛ける企業で、国内ではEE Tech Focus社が代理店である。

フォーマル検証ツールは、シミュレーションのようにスティミュラスに依存する検証ではなく、デザインが取り得るすべてのステートが、仕様を元に作成されたプロパティに対して違反がないかどうかを網羅的に検証する。その網羅性によってデザイン正当性の確信が得られるため、近年ではフォーマルサインオフへの期待が高まる一方で、実際のプロジェクトでは適用が難しいと聞く。

インタビューでは、Axiomiseの特徴と実績を中心に話を聞いた。

画像はAxiomise社 CEO Ashish Darbari氏

Axiomiseという会社について、そしてAshishさんがAxiomiseのCEOとして成し遂げたいことについて聞かせてください。

Axiomiseはフォーマル検証のコンサルティングや検証サービスを提供する企業ですが、トレーニングや“making formal normal” というフレーズの元、フォーマル検証の普及に注力しています。私たちの夢やビジョンは、フォーマル検証を主流にし、シミュレーションによる検証を補完できるようにすることです。

その実現方法の一つとして、コンサルティングやサービス提供を通じて実践的なプロジェクト作業を継続し、半導体設計企業の全エンジニアをトレーニングで支援すること、そして必要ならば当社の強力なツールやソリューションを提供して加速します。つまり全体として、フォーマル検証をより一般的な手法にすることが目的で、私の長年の夢でもあります。

フォーマル・プロパティ・チェッキングは、一般的に適用が難しいと聞いています。エンジニアがプロパティを記述しなくてはならず、プロパティの妥当性や網羅性など、決まった手法というよりも属人性の要素がある気がします。また扱える設計規模にも限界があると聞きます。このような課題に対して、Axiomiseはどのようにアプローチするのでしょうか。

素晴らしい質問です。これは私が言うところのフォーマル検証のスケーラビリティの限界です。かつてはフォーマル検証にその限界があると認識されていました。しかし2025年の現在、ツールは20～30年前とは大きく異なります。とは言え、設計規模は拡大し、市場投入までの時間は短縮され、設計の複雑度は上がり、依然としてスケーラビリティの問題を抱えています。この課題の克服は、仕様をインテリジェントな機械可読な形式で記述し、抽象化テクニックや問題最小化の戦略を適用することです。これによってフォーマル検証の究極的な目標である構造的推論を容易に実現できます。これらのテクニックを適切に導入すれば、特にフォーマル証明の達成において、フォーマル検証の威力を格段に引き上げることができるのです。

そしてデバッグも重要で、検証作業時間の多くの時間がデバッグに費やされる現状を踏まえ、その高速化に取り組んでいます。デバッグを自動化し、バグの根本原因を迅速に抽出する必要があります。最終的には完全な多次元のカバレッジビューを用いて検証を完了させ、サインオフします。つまり抽象化、仕様定義、問題の最小化といったところから開始し、高速かつ効率的なデバッグ作業を継続してカバレッジで完結させます。この一連のフローが確立されれば、フォーマル検証は実践において非常に容易でかつ扱いやすい手法となります。

コンサルティングやサービスを通して、これまでフォーマル検証を活用したプロジェクトはいくつぐらいありますか？

Axiomiseでは過去8年間で、25以上の異なる複雑さのプロジェクトを扱ってきました。その大半はプロセッサで、RISC-V、GPU、機械学習アクセラレータチップ、あるいはNOCやネットワークチップに関するものでした。私の25～30年の経験では、個人として、または他チームを支援することで100件近く、エンドツーエンドの高品質な検証を達成しています。

UVMなどシミュレーション・ベースで検証する場合、第三者の視点を持つ検証エンジニアが組織化されているプロジェクトもあります。フォーマル検証でコンサルティングをする上で、シミュレーションと比較して気をつけているようなことがあれば、教えてください。

私たちはコンサルティングや検証サービスを提供する企業ですから、基本的にはお客様の組織の延長として参画します。お客様は自社の設計チームや検証チームがあり、仕様書もあります。そこに我々の精鋭チームが実際に参画し、エンドツーエンドのフォーマル・テストベンチを構築し始めます。

我々が扱う非常に複雑な設計に対するテストベンチ作成作業は膨大な人的労力を要します。現在AI技術を導入しつつあり、当社からもお客様からも労働集約的な作業を取り除くことを目指しています。このような作業をよりインテリジェント化しようとしていますが、同時に顧客の要求の変化、優先順位の変化、仕様や設計の変更に対応することも極めて重要です。

当社のエンジニアはこうした変化に対応可能です。UVMテストベンチではデザイン固有の独自スクリプトを作成しますが、我々も同様の哲学を踏襲しています。コードからデバッグ、サインオフフロー、レポートフローに至る環境を完全にカスタマイズできます。さらに自動化を推進し、より高度なカスタマイズを実現していきます。

フォーマル検証を適用するメソドロジとして、Axiomiseに特徴的なものやこだわりはありますか？

プロジェクトでは開始点と終了点が非常に重要です。プロジェクトの初期段階では、仕様や設計属性のニュアンスや複雑さを把握し、主にアーキテクチャ的側面とマイクロアーキテクチャ的側面を理解します。そして検証用のフォーマル・テストベンチを実際にどう適用させるかを検討します。この初期段階で明確な理解が得られれば、どの抽象化テクニックや問題最小化テクニックを導入すべきかを判断できます。これが素晴らしいスタートポイントとなります。

次にインコンクルーシブ、つまり不完全な証明に備える必要があります。そこで証明のためのエンジニアリングフローを構築し、網羅的に証明します。ここで高い網羅性を確保するというこの理想こそが、Axiomiseの最大の「独自の売り」です。しかし同時に証明そのものが最大の価値ではありません。設計者が十分な確信を得られるよう、継続的にバグハンティングを行い、最終的にカバレッジを提供しなくてはなりません。この全体像が重要なのです。

フォーマルアプリも提供されているということですが、どのような種類がありますか？ またそれはEDAベンダーがリリースしているものと何が違うのでしょうか？

私たちは機能検証の領域で、主にフォーマルプロパティを手段としており、通常であればシミュレーションで行うような検証の重積を全て担っています。必要に応じてシミュレーション検証をフォーマル検証に移行します。その過程で、より洗練され高速な手法を模索してきました。

RISC-Vのような特定ドメイン向けには、専用アプリ - formalISAを開発しました。オープンソース／商用を問わず15～18種類のプロセッサに適用されており、RISC-Vでシリコンを起こす企業がフォーマル検証の高速化、網羅的証明、バグハンティング、カバレッジ向上を確実に得られるよう設計されています。これは主にRISC-Vの市場がターゲットです。

同時に、より汎用性の高いPPA（電力・性能・面積）の問題やデータパスのドメインにも取り組んでいます。データパスはAIチップの機械学習アクセラレータやキャッシュサブシステムの中核を成します。我々はかなり大規模なメモリサブシステムの検証にも相当な期間取り組んできました。目指しているのは、可能な限り自動化を進め、毎年繰り返される単純作業を削減することです。

ファブリックの接続性の問題にも取り組んでいます。大規模なNetwork On Chip設計の検証も行っており、その処理速度の向上も模索中です。現時点でAxiomiseはRISC-V向けformalISAと、ほぼ全てのシリコン設計に対応するfootprintを提供しています。今後の展開にもご注目ください。間もなく新アプリケーションをリリースし、来年も継続的に展開していく予定です。

フォーマル検証のコンサルティングやサービスをする会社が、アプリケーションまで開発をするのは何故ですか？

また素晴らしい質問ですね。先ほども述べた通り、私たちがフォーマル検証に取り組む理由はフォーマル検証を日常的なものにし、高速化・高品質化を図り、市場投入までの時間を短縮するためです。品質と市場投入までの時間を考慮すると、これを実現する唯一の方法は、困難な問題を自動化されたソリューションで解決可能にすることです。人的要素を排除することでエラー発生率を低減し、より多くのエンジニアが確実に、仕様ミスやコードエラーを犯すことなく、フォーマル証明を達成できる形を目指しています。

これは当社にとって極めて自然な次の進化段階です。何千人もの人員を要する労働集約型の企業を目指すつもりはなく、より知的に業務を遂行し、顧客にソリューションのカスタマイズ選択肢を提供したいと考えています。

これを実現する唯一の方法は、専用ソリューションを通じたアプローチです。シリコンはカスタマイズ化が進んでいます。機能検証も同様にカスタマイズ化が必要です。そこで過去1年半、私たちが掲げてきた指針は「シリコンのカスタマイズ化が進む中で、検証をどうカスタマイズするか」でした。シリコンはもはやx86やARMアーキテクチャだけではなく、完全にヘテロジニアスになっています。カスタマイズされたシリコンの微細な側面を理解しつつ、即効性のあるソリューションを提供する必要があります。

DVCon Japanへの出展は昨年に続いて２度目になります。成果は得られましたか？

日本は本当に素晴らしい国です。前回は当社初の、私自身も初めての日本訪問でした。これほどまでにユニークな国は見たことがありません。DVCon Japanは、DVConが年間を通じて世界各地で開催されるカンファレンスシリーズの一環です。私たちは米国、インド、欧州では既に積極的に参画しています。日本については、プロジェクトの多さ、技術革新の多さから、以前から来日すべきだと考えていました。DVConの実行委員会からも強く促され、ここに来るべきだと決断しました。

そしてこの2年間、素晴らしい経験をしました。私が学んだことの一つは、これほど短期間で、これほど狭い地域に、これほど多くの技術を集中させている国は他にはないということです。例えばカメラを製造する企業、映像機器を製造する企業、自動車用チップを製造する企業などが存在しています。当社が日本進出を検討し、実際に参入するまでにこれほど時間を要したのは、判断の遅れだと思います。逆に、今まさに大きな期待を抱いています。数多くの企業と協議を重ね、エンジニアが設計段階で直面する課題を理解しようとしています。

日本には自動化への強い志向がありますね。日本の文化には、自動化をさらに推進するという概念が根付いていると見ています。これまでの2度の訪問で学んだのは、日本の半導体設計会社が直面する課題を解決するには、こうした自動化をより効果的に実現するツールを構築するということです。

日本国内のお客さんに対してコンサルティングやサービスを提供する際、言葉の壁が問題になることはありませんか？

言語はあらゆる文化に内在する重要な要素だと思います。日本の文化に関しては、人々が多少の英語を話すとはいえ、日本語のコミュニケーションのニュアンスを理解できることが重要だと気づき始めています。その点については取り組んでいきたいと思っています。しかし、これまでのところ、日本で協力している販売代理店のおかげで、実プロジェクトにおけるコミュニケーションに大きな障壁は生じていません。

お忙しいところお話しを聞かせて頂きありがとうございました。フォーマル検証は使い方が重要、その運用方法が成否を左右することをあらためて実感しました。Axiomiseのノウハウが日本の設計プロジェクトにも活かされることに期待します。

※Axiomise

※Axiomise 日本代理店 EE Tech Focus合同会社　

お問い合わせ： 三橋 明城男 akio_mitsuhashi@eetechfocus.com