【48DAC】初出展のOski、フォーマル検証はノウハウ次第でもっと効果が上がる

第48回Design Automation Conferenceに出展していたOski Technologyのブース・レポート。

Oski Technologyは、2005年設立のEDAベンチャーで今回が初のDAC出展。本拠地はマウンテンビューでインドにもオフィスを構える。CEOのVigyan Singhal氏は元Jasper Design Automationのエンジニアで、Jasperへのリスペクトの表れか社名ロゴや配色がどことなくJasperに似ている。

同社はフォーマル検証にフォーカスした検証サービスを手掛ける会社で、製品は提供していないがフォーマル検証最適化のためのIPと呼べる「Oski's Abstraction Models」という内製モデルを持っている。

Vigyan Singhal氏によると、同社のサービスは使用しているフォーマル検証を問わず、フォーマル検証のTAT短縮とカバレッジ向上を実現するもので、確立された独自の検証メソドロジによって検証時間を概ね半分に減らす事が可能。具体的には、CとRTLのシーケンシャル等価性検証やRTLのプロパティ検証の最適化に対応しており、大規模かつ複雑なデザインにも対応できるという事。具体例として聞いたのは、バスブリッジの検証やメモリ・コントローラIPの検証における効果で、それぞれ検証工数の削減やカバレッジホールの削減に成功したという。

尚、同社は未だ日本には営業ルートが無く良いパートナーを探しているとの事。北米ではXilinx、NVIDIA、Ciscoといった大手の他に新興FPGAベンダのTabulaなどにもサービスを提供しているという。

※Oski Technology