フォーマル検証サービス

抽象化ドリブン

スケーラブルなソリューション

SoCのエンド・ツー・エンドのサインオフ

RISC-V フォーマル検証

オンデマンド・トレーニング

インストラクタによるトレーニング

Making formal normal

私たちは、常に電子チップに囲まれています。携帯電話であれ、ノートパソコンであれ、スマートウォッチであれ、自動車であれ、飛行機であれ、半導体が世界を動かしています。半導体集積回路（IC）設計を原動力とする電子チップと、その基盤となるソフトウェアへの依存度は、かつてないほど高まっています。

航空宇宙、ヘルスケア、自動車から、インテリジェントなAI/MLを搭載した家電製品、電力網に電力を供給する産業用プロセス制御システムまで、IC設計はあらゆるところに存在し、これらに不具合や欠陥が生じることは許されません。Ariane 5やIntelのFDIVの不具合、つまりMeltdownやSpectreなどのセキュリティ欠陥など、ダイナミックなシミュレーションに基づくASICやFPGAの機能検証は困難を極めています。

機能安全やセキュリティの要件を考慮すると、従来のシミュレーションベースの検証では保証を提供することに無理があります。バグがないことを保証する唯一の方法は、正しさを数学的に証明することで、フォーマル手法によるのです。

Axiomiseのビジョンは、フォーマルをノーマルにすることであり、過去6年間、私たちはまさにそれを実践してきました！

当社は2017年以来、半導体業界におけるフォーマル検証の導入のパイオニアです。 フォーマル検証で63件の特許を持つビジョナリー、CEOのDr. Ashish Darbariと40年の経験を持つ業界のベテランであるNeil Dunlop氏が率いるAxiomiseは、トレーニングプログラム、コンサルティング＆サービス、RISC-Vプロセッサのエンドツーエンド検証のためのベンダーニュートラルなフォーマル検証アプリを通じて、最先端のフォーマル検証メソドロジへのアクセスを提供し、過去6年間で20社のお客様を支援してきました。

当社は、あらゆる商用フォーマル検証ツールで使用可能な抽象化ドリブンのメソドロジと6次元カバレッジソリューションにより、複雑なSoCへのフォーマル手法の導入を容易にしています。Axiomiseのエキスパートは、RISC-V、Arm、x86プロセッサ、GPU、ビデオブロック、WiFiや5Gを含むネットワークブロック、AI/MLハードウェア、NoCベースのファブリックなど、最も困難なフォーマル検証問題に取り組むことができます。

当社は、通常の機能検証の課題だけでなく、安全性が極めて重要でセキュリティが重要な検証タスクにおいてもお客様を支援し、検証済みの設計においてもバグを発見し、バグが存在しないことを徹底的に証明します。

Axiomiseは、20年以上にわたり産業界とトップクラスの研究所でフォーマル検証の導入を推し進めてきたDr. Ashish Darbariによって2017年に設立されました。Axiomiseでは、すべての半導体設計検証においてフォーマル手法を主流にする唯一の方法は、フォーマル手法のエンドユーザーである半導体業界の何百人もの設計者や検証エンジニアを支援し、育てることであると考えています。2022年、Dr. DarbariにNeil Dunlop氏が加わりました。NeilとAshishの2人によって築かれたAxiomiseのリーダーシップチームは、60年以上ものプロジェクトにおけるフォーマル検証の経験値を有しており、これは世界のどこにもありません。

Axiomiseは専門用語を単純化し、Axiomiseの抽象化ドリブンのメソドロジによって複雑な問題がいかに簡単に解決されるかをお客様のプロジェクトでお見せすることで、フォーマル検証の導入を可能にしています。 Axiomiseのソリューションがどのようにトップクラスの半導体デザインハウスを支援しているか、またAxiomiseがどのようにお客様やお客様のチームにとってフォーマル検証をノーマルなものにできるか、ぜひご相談ください。私たちは、バグを発見し、バグがないことの証明を築くためにformalISAと呼ばれる自動フォーマル検証アプリを展開するだけでなく、過去6年間に数多くのお客様のプロジェクトを支援し、業界全体で300人以上のエンジニアをトレーニングしてきました。

フォーマル検証で質の高いサインオフを実現するための予測可能な適用方法を学びましょう。私たちと一緒に仕事をすれば、フォーマルの虜になるに違いありません！