Summary - CadenceCONNECT: Jasper User Group Japan 2026

毎年恒例のフォーマル検証テクニカルカンファレンス「Jasper User Group Japan 2026」を開催いたします。

本イベントでは、Jasperユーザーの皆様による活用事例や成功事例をご紹介するとともに、ケイデンスの最新のフォーマル検証技術、検証手法、ソリューションに関する情報をお届けします。
すでにフォーマル検証をご活用いただいているエキスパートの方はもちろん、これから導入をご検討される方にも、実践的な知見や最新情報を得ていただける機会です。

ぜひ「Jasper User Group Japan 2026」にご参加いただき、設計・検証プロセスのさらなる効率化や、今後のプロジェクトに役立つヒントをお持ち帰りください。

主　催：　日本ケイデンス・デザイン・システムズ社
　　　　イノテック株式会社　ICソリューション本部
日　時： 12月4日（金）13:00-19:00予定（17:15～19:00懇親会）受付開始：12:30
会　場：東京コンファレンスセンター・品 JR品川駅港南口（東口）より徒歩2分
参加費用：　無料
登録締切：　12月2日（水）　17:00

※ 例年と会場が異なりますので、お間違いのないようご注意ください。

13:05～14:05　ケイデンス・キーノート： Unleash Jasper: Trusted Agentic Formal at Scale

これまでFormal Verificationの適用規模は、Formal Expertが対応できる範囲に制約されてきました。しかし、Agentic AIにより、その限界を大きく超えることが可能になりつつあります。

本講演では、Jasper APIと専門的なSub-agent群を基盤とするChipStack Formal Agentが、Formal Verificationをより多くのユーザーに広げるとともに、Formal ExpertがSignoffまで対応できるDesignの範囲をどのように拡大するのかを紹介します。

一方、このような規模でAIを活用するには、結果に対する信頼が不可欠です。AIがより複雑な問題に適用され、基盤となるLLMも進化し続ける中で、一貫した信頼性を維持することは容易ではありません。

本講演では、Jasperが20年以上にわたって培ってきた信頼性の基盤をAgentにも継承することで、LLMが変化しても一貫した結果を維持し、長期にわたって信頼できるFormal Verificationを実現する方法を紹介します。

米国ケイデンス・デザイン・システムズ社
Chris Komar, Sr Product Engineering Group Director

14:10～14:50　Formal検証の収束性向上を目的としたFormal-Oriented Designの提案と
I/F IPにおけるFormal Signoff事例

Formal検証は強力ですが、収束性等に課題があります。本発表では、Formal検証を収束させることに主眼を置いた設計であるFormal-Oriented Desing(FOD)を提案します。本手法では、機能分割や状態・パイプライン構造を工夫し、収束性を向上させます。本発表では、FODを実開発に適用し、Formal Signoffを実現した事例を紹介します。

ルネサスエレクトロニクス株式会社
エンジニアリンググループデジタルＩＰ開発統括部高速Ｉ／Ｆ技術開発部

溝口大介氏、入倉直輝氏

14:50～15:30　設計・検証現場におけるJasper活用の段階的定着アプローチ
― 運用自動化・回路複雑度解析・仕様構造化への展開 ―
　　　　　　　　

フォーマル検証を開発現場に定着させるため、私たちは組織と技術の両面から改善を進めてきました。
検証結果を解析して回路を改善することに設計者が集中できるよう、実行を担う専門チームの設置や自動化、制約条件の資産化を進めてきました。
また、より根本的な回路改善に向け、回路複雑度の分析やアサーション適用に向けた仕様の役割整理・記述見直しなど多面的な取り組みも進めています。
本講演では、段階的な実践と試行錯誤をご紹介します。

三菱電機株式会社
設計技術開発センター LSI応用技術部デジタル回路機能集約技術二グループ
三輪昌伸氏

15:50～16:30　Formal Expertが試す ChipStack Formal Agentの実力
　　　　　　　　

Formal検証は強力な手法として知られていますが、環境構築やアサーション記述の難しさから、設計者への展開は容易ではありません。
本発表では、Formal ExpertがChipStack Formal Agentを用いて、RTL（約7,200行、仕様書62ページ）を対象に行った評価事例を紹介いたします。
メンタルモデルの生成、環境構築、反例解析での試行錯誤や工夫を通して見えてきた活用のコツを共有し、「Formal検証初心者でも実用的なFormal検証は可能なのか」を考察します。

日本ケイデンス・デザイン・システムズ社
フィールドエンジニアリング＆サービス本部　システム&ベリフィケーション　
テクニカルリーダー　田口光宏

16:30～17:10　フォーマル検証初心者によるDesign for Verification実践
　　　　　　　　

近年、イメージセンサの高機能化・複雑化に伴い、開発期間の長期化や不具合の増加が課題となっています。
本発表では、これらの課題解決に向けて取り組んだ、実装性とフォーマル検証容易性を両立したデジタル回路アーキテクチャの開発について紹介します。
また、その過程で直面した課題と解決策、得られた成果・効果に加え、今後の展望としてAI活用を見据えた将来計画についてもご紹介します。

ソニーセミコンダクタソリューションズ株式会社
イメージングシステム事業部 IS設計1部　宮田慎也氏