形式検証エンジンは「証明済み」と告げた。それでもチップは壊れていた。
私たち自身のツールが初めて私に嘘をついたとき、それは礼儀正しくそうした。形式検証エンジンは緑のチェックマークを返した。私たちが証明を求めたすべてのプロパティは、証明済みとして返ってきた。アサーションライブラリは完全に見えた。書類上、その設計は検証済みだった。
その証明書が無価値であり、そして私が半導体AI検証について想定していたすべてが間違った失敗から私たちを守っていたのだと気づくまでに、二日かかった。
そのプロパティは、私たちが形式検証エンジンにかぶせた大規模言語モデルによって生成されていた——まさに誰もが作っていた、洗練されたエージェント型チップ設計デモそのものだ。そしてエンジンはそれらをミリ秒で証明した。それこそが手がかりであるべきだった。それらが証明されたのは、それらを試すはずの条件が一度も発火しなかったからだ。「すべてのリクエストはいずれ許可を得る」と述べるプロパティは、リクエストが決して起こり得ないなら自明に真である。ソルバーが間違っていたわけではない。私たちがうっかり尋ねた問いに答えただけで、その問いは空だったのだ。これらのAI検証パイプラインが実際に何から身を守らなければならないのか——そして、それを売るほぼ誰もが正しいものから守っていなかったのはなぜか——を私が理解したのは、その瞬間だった。
私たちが見つけたことをお伝えしたい。というのも、現代のチップを死に至らしめるバグの種類は、業界が捕捉できると宣伝しているものではないからだ。私たちはファブレスのチップチームのためにカスタム検証パイプラインを構築している——チームがすでに所有する形式検証エンジンにかぶせた、ファインチューニング済みのオープンウェイトモデルで、すべて自社のハードウェア上で動く——そして、このアプローチ全体は、まずこれを間違えたことから生まれた。その全体像は次で見ることができる。veriprajna.com/solutions/semiconductor-ai-verification。だがこのアプローチは、「合格」した設計が失敗するのを目にして初めて意味をなす。
すべてのファブレスCFOを震え上がらせるべき数字
一つの統計が問題全体を枠づけている。2024年のWilson Research Group / Siemens EDA機能検証調査——業界で最も長く続くベンチマーク——は、初回シリコン成功率を14%とした。追跡してきた二十年で最も低い数字だ。2020年にはその数字は約32%だった。四年で半分以下になったのだ。
これはエンジニアが怠けているという話ではない。複雑さがツールを追い越しているという話であり、仕様が、それを追うテストベンチよりも速く変化しているという話だ。同じ調査は、およそリスピンの70%は仕様変更に結びついたエラーによって引き起こされることを見出した——純粋なロジックバグではなく。
初回シリコン成功率が下がったのは、チップチームの質が落ちたからではない。今や仕様が、検証がそれを締め切れるよりも速く動くから下がったのだ。
私はその70%という数字を長いあいだ噛みしめた。というのも、それは多くの「チップ設計のためのAI」という売り込みを静かに告発しているからだ。もしリスピンの大半が仕様のドリフトから来るのなら、ロジックバグしか捕捉しないツールは、問題の一切れに取り組んでいるだけなのに、それをパイ全体だと称していることになる。
そして、間違えることのコストは、ソフトウェアの人々が過小評価するほど残酷だ。5nmのマスクセットは$10–20Mかかる。3nmでは$40Mに迫り、二十を超えるEUV層を含む七十以上のマスク層になる。フルの2nmテープアウトは今や、総額で$725Mのオーダーになる。何かがすり抜けると、リスピンはマスク費用に加えて3〜6か月のスケジュール遅延となる。十八か月の製品ウィンドウでは、六か月の遅れがチップの生涯収益の半分を消し去りかねない。CFOは検証をコストセンターとは見ていない。彼らはそれを、一度の八桁の間違いに対する保険と見ている。
LLMはハードウェアで実際にどうハルシネーションを起こすのか？
あなたのチームはすでにVerilogでLLMを使っている。私はそうでないふりをするつもりはないし、あなたに売り込む者も同様にすべきだ。この研究分野は今や本物だ——LLMがVerilogを書くことに関する論文は、2020年の1本から、2025年には64本へと増えた。VerilogEvalベンチマークのより難しい問題では、GPT-4クラスのモデルは機能的正しさで約43%に着地する。有用だ。だが信頼はできない。
興味深い問いは、モデルが役に立つかどうかではない。それは、どのように失敗するかだ。というのも、その失敗のしかたは、ソフトウェアエンジニアが恐れるよう訓練されている失敗には見えないからだ。「正しく見える」RTLがなぜ間違ったのかを見つめる夜更けを十分に重ねたあと、私は失敗を五つの分類に整理し始めた。
最初のものは無害なものだ。構文的なハルシネーション——単にコンパイルできないコードだ。Verilatorや合成のフロントエンドが数秒で捕捉する。誰もがすでにこれの扱い方を知っており、問題は解決済みだと主張したいときに人々が指し示す分類だ。
二つ目は、痛み始めるところだ。意味的なハルシネーションで、教科書的な事例はブロッキング代入と非ブロッキング代入の対比だ。PythonとCで訓練されたモデルは、Verilogを、文が上から下へ実行されるかのように読む。そこでモデルは、ブロッキング代入——単なる=——を、クロック同期のalways_ffブロックの中に書いてしまう。そこは言語が非ブロッキングの<=を要求する場所だ。設計者は二段のパイプラインを望んでいた。ブロッキング代入では、第二段は第一段の新しい値を読み、古い値ではない。そして、シリコンは代わりに一サイクルのバイパスを出荷してしまう。一部のシミュレータは、そのレースを完全に隠す順序でイベントをスケジュールする。シミュレーションでは問題なく動く。だが合成すると間違ったマシンになる。
三つ目の分類は、AMBA仕様を第二のモニターに開いておくよう私に教えたものだ。プロトコルハルシネーションだ。コードはコンパイルされ、指示されたテストの九割に合格し、そしてスレーブがアドレスを受け入れる準備が整う前にwrite-data-valid信号をアサートする——AXIハンドシェイクの違反だ。あるいは、valid信号をハイに保ったまま、その下でデータを反転させる。あるいは、どの人間も暗記していない、バス仕様の84ページに埋もれたサブ条項を踏んでしまう。そのチップはあなたの内部テストハーネスでは完璧に動き、サードパーティのメモリコントローラに配線された瞬間にハングする。これはシミュレーションサイクルを増やしても力任せには解決できない。各プロトコルに対して書かれた、事前検証済みのアサーションライブラリで捕捉するのだ。
四つ目の分類は、私たちを欺いたものであり、危険なものだ。
なぜ「証明済み」は検証レポートで最も危険な言葉なのか？
空虚性のハルシネーションだ。モデルはSystemVerilogのアサーションを生成する。形式検証エンジンはそれを証明する。あなたは出荷する。だが、そのプロパティが自明に真だったのは、その前件——「もし」の部分——がそもそも一度も真にならなかったからだ。
アービタのプロパティを思い描いてほしい。リクエストが立てば、ある数のサイクル以内に許可が続かなければならない。さて、同じモデルが、役に立とうとして、リクエスト信号をローに固定する仮定も書いたとしよう。形式検証エンジンは、それを違反しうるリクエストが存在しないため、許可のプロパティを律儀にミリ秒で証明する。その下にある本物のアービタは、完全に壊れているかもしれない。証明書には「証明済み」と書かれている。それは無価値だ。
ミリ秒で走る形式証明は、速いのではない。怪しいのだ。エンジンは何一つ証明していないかもしれない。
これは周縁的なリスクではない。Siemensは2017年から空虚な証明についての警告を公表しており、それでもこの分野は自動の空虚性チェックのないフローを出荷し続けている。空虚性検出のない形式検証フローは、形式検証がないよりも悪いと私が人々に言うと、彼らは私が大げさだと思う。そうではない。検証がなければ、あなたは相応に怖がっていられる。空虚な「証明済み」は、サインオフされたブロックをテープアウトへ向かわせながら、あなたを自信満々で、しかも間違ったままにする。それが、私たち自身の初期プロトタイプで危うく出荷されかけた失敗であり、私たちが作るものを永久に変えた。
五つ目の分類は、シミュレーションが構造的に見ることのできないものだ。クロックドメインクロッシングの盲点だ。LLMは信号名を読むが、クロックドメインを知覚しない。そのため、メタスタビリティを防ぐダブルフロップの同期回路を飛ばして、2GHzのCPUドメインの信号を400MHzの周辺ドメインのフロップに直結してしまう。RTLシミュレーションはメタスタビリティをモデル化しない——だから回帰テストは毎回合格し、そしてシリコンは現場でデッドロックする。これがCDCバグがマスクセットを食い潰す理由だ。またそれは、Accelleraが2024年にCDC/RDC相互運用性標準を立ち上げた理由でもある——商用CDCツール間の断片化が、サインオフを壊すほどひどくなっていたのだ。
二つ目から五つ目までの分類は、一つの恐ろしい性質を共有している——それらはシミュレーションに合格する。それらはシリコンでしか表面化しない。それが、いまだにテープアウトを吹き飛ばすバグの部分集合であり、まさに「ロジックバグを捕捉する」という売り込みが取りこぼす部分集合だ。
チップチームが実際に立ち向かっているベンダーの壁
テープアウトについて真に独立した助けを探しに行ったとき、私が見つけた選択肢は、数年前に持っていたよりも少なかった——そしてそれはノスタルジアではなく、市場構造だ。設計検証のリードが実際に選べる三つのEDAベンダー——Synopsys、Cadence、Siemens——は、十年前の市場の75%未満から、今日の85%超へと拡大した。Synopsysの$35BのAnsys買収を織り込めば、上位四社がおよそ90%を支配する。ファブレスのスタートアップが買い物をする分野は、問題が難しくなったのとまさに同時に、広がるのではなく狭まったのだ。
そして既存勢力はAIで立ち止まってはいない。Synopsysは2026年3月にAgentEngineerを出荷した。二〜五倍の生産性をうたうエージェント型の検証ワークフローで、VC Formalの上に載っている——私が評価したなかで最も信頼できるベンダーのエージェント型スタックだ。Cadenceは2026年2月にChipStack AI Super Agentを発表し、強化学習駆動の実装のためにCerebrus AI Studioを動かしている。JasperGoldは、他のすべてが比較される金字塔的な形式検証エンジンであり続けている。私はこれを曖昧にせずに言う——JasperGoldとVC Formalは本当に優秀だ。それらをこき下ろすことから売り込みを始める者は、本物のテープアウトを一度も締めくくったことがないと白状しているのだ。
落とし穴は価格と姿勢だ。JasperGoldの歴史的なベースラインは、およそ$225Kに加えて1席あたり$45Kで走っていた——大規模なファブレス企業には問題ないが、最も興味深い仕事をしている初期段階のRISC-VやAIアクセラレータのスタートアップには手が届かない。そして既存勢力の最新のAI機能はクラウド優先であり、これらの顧客が決して曲げない唯一の要件と真正面から衝突する。それについては、この後すぐに述べる。
次にスタートアップの波があり、それは騒がしい。前回のDACとDVConでは、私が一緒に仕事をしているあるDVリードが、たった一四半期で八つもの異なる「チップ設計のためのエージェント型AI」企業から売り込みを受けていた。ChipAgentsは2026年初頭時点で$74Mを調達し、十倍の設計・検証生産性をうたっている。Normal ComputingはSamsungのCatalyst Fundが主導する$50Mを調達し、自動形式化——エンジニアの意図を直接、形式的プロパティへと翻訳して証明するLLM——を構築しており、世界の半導体設計企業トップ10の半分が使っていると言う。ほかにもある——MooresLabAIは完全なテストベンチを生成し、Broncoは回帰解析、Silimateは電力・性能・面積の予測を扱う。
これらの一部は本物だ。だがどれも顧客の実際の問題を解決しない——顧客は今やこうしたポイントツールを三つ買ってしまい、すでに信頼しているサインオフのフローの中でそれらをどう連携させればよいのか、まったく見当がつかないのだ。
誰も声に出して言いたがらない、強化学習による配置の物語
チップ設計には、検証を越えたところに並行する誘惑がある——強化学習を使って物理的なフロアプランニング、つまり大きなブロックがダイ上のどこに座るかを決めることだ。それは魅力的で、最も引用される結果は、大半の売り込みが都合よく飛ばす形で論争になっている。
2020年のGoogleのNature論文は、マクロ配置において強化学習がシミュレーテッドアニーリングを上回ると主張し、それは実際のシリコンで使われた——複数世代のTPUがそれを搭載して出荷された。だが2023年、方法論上の懸念が提起されたのを受けて、Natureは編集上の注記を追加した。現在Synopsysにいるイゴール・マルコフは、その見出しとなる比較が目に焼き付いて離れない、一行ずつの批判を公表した——強化学習のアプローチは32.31時間、チューニングされたシミュレーテッドアニーリングのベースラインは12.5時間、そして商用のCadenceツールは同じ仕事を0.05時間で終えた。DeepMindは「That Chip Has Sailed」と題した論文で反撃した。何年経っても、独立した外部の再現は元の主張を確認しておらず、批判と反論はどちらもいまだに継続中だ。
私がこれを持ち出すのは、コンサルタントが本物の形式検証チームにRL配置を売り込み、その論争が存在しないふりをするとき、何が起こるかを知っているからだ。彼らは十分以内にそれを嗅ぎつけ、あなたはその場を失う。正直な立場は、真のニッチが存在するというものだ——チップレットや3D-ICの熱を考慮したフロアプランニング、アナログレイアウト、オープンなツール上でのRISC-V IP最適化——そこではハイブリッドなアプローチがその価値を稼ぐ。既存勢力の配置エンジンへの正面攻撃は、そうはいかない。その違いを知り、それを声に出して言うことこそが、仕事のすべてだ。
私たちのツールが私たちを欺いたあと、何が変わったか
そこで、この空虚な証明の災難が私たちを導いた先はこうだ。私たちは、Verilogを書くより優れたAIを作ろうとするのをやめた。それは資金を得た八人の走者がひしめくレースだからだ。そして、彼らの誰も売っていないものを作り始めた——ベンダー中立の統合レイヤー、チームの既存ツールを信頼できるものにするものだ。
具体的には、それはいくつかの決定を意味し、そのそれぞれが、私たちが目にした失敗によって強いられたものだ。私たちはオープンウェイトのモデル——Qwen Coder、Llama、どれでも合うもの——を、顧客自身のRTLコーパス、彼らの仕様、彼らの過去のバグ履歴でファインチューニングする。なぜなら、あなたのハウススタイルを見たことのないモデルは、それに対してハルシネーションを起こすからだ。私たちはそれを、チームがすでに所有するどんな形式検証エンジンにもかぶせる——JasperGold、VC Formal、Questa Formal、あるいはオープンソースのSymbiYosys。私たちは、彼らがすでに信頼している金字塔的なツールを引き剥がすよう求めることは決してない。そして、モデルが提案するすべてのプロパティは、誰かが「証明済み」という言葉を読むことを許される前に、空虚性とカバレッジのチェックを通過する——なぜなら私たちは、防護のない証明は芝居だということを、高くつくやり方で学んだからだ。
事前検証済みのアサーションライブラリは、モデルと同じくらい重要だ。RISC-Vコアには、形式検証ハーネスがAXI4、AHB、TileLinkの適合性チェック、パイプラインハザードのアサーション、ロードストアのスコアボーディング、デバッグユニットの正しさに関するプロパティを備えて出荷される——プロトコルおよび意味的ハルシネーションを、シリコンより先に捕捉するものだ。これは机上の空論ではない。形式検証のコンサルタント会社Axiomiseは、Ibexで65個以上のバグを発見した。IbexはGoogleのOpenTitanの中にあるオープンなRISC-Vコアで、その中には形式検証だけが捕捉できたデバッグユニットの分岐命令バグも含まれる。形式検証はRISC-Vで機能する。希少なのは手法ではない——それを使いこなす術を知るチームだ。
ここでの本当の突破口は、より賢いVerilogモデルなどでは決してなかった。それは、チームがすでに信頼している高価なツールにかぶせた、正直なハーネスだった。
なぜクラウドで走らせるだけにしないのか？
人々は絶えず私にこれを尋ねる。そしてその答えは、あらゆるクラウド優先のEDA-AIスタートアップが、私が大切に思う顧客のもとでは到着時に既に死んでいるのと同じ理由だ——RTLは至宝であり、建物の外には出ない。
ファブレス企業のレジスタ転送レベルのコードは、その企業そのものである。防衛や航空宇宙の顧客は、それをエアギャップで隔離することを、時には安全な施設内で必要とする。商用のファブレスチームは、絶対的な最低限としてオンプレミスか、仮想プライベートクラウドを望む。だから私たちはすべてを顧客自身のハードウェア上で走らせる——既存のH100やH200クラスタでのvLLMや同様の推論、自社コーパスに対するローカルな検索、そしてRTLがネットワーク境界を越えることは決してない。既存勢力の最新のエージェント型機能はクラウド優先だ——それは彼らにとっては機能だが、IPに敏感なチップチームにとっては論外だ。私が見る最大の突破口は、まったくアルゴリズムの問題ではない。それは、最良のアルゴリズムを持つ人々が解決しないと決めた、デプロイと統合の問題だ。
もう一つの問いは自動車チームから来るもので、彼らにとってすべてを決める問いだ。ASIL CまたはDで車にチップを載せる——ISO 26262が形式検証を単に提案するのをやめ、それを義務づけ始める安全度水準だ——と、ツール自体がTCL2またはTCL3の認定パッケージを備えていなければならない。既存勢力のコアエンジンはそのサードパーティ認証を持っている——真新しいAIツールは持っていない。私は、まさにこの理由で、本当に優れたツールが自動車プログラムでベンチに下げられるのを見てきた——認定パッケージがなく、サインオフのフローに居場所がなく、会話は終わり。だから私たちは、認定されたツールになろうとはしない。私たちは、認定チェーンを壊さずに、認定された既存エンジンと並べてAIの支援を走らせる手助けをする——なぜなら自動車では、監査を生き延びられない技術的に優れたツールは、何の価値もないからだ。
証明書はチップではない
私は、何の意味もない緑のチェックマークを信じて費やしたあの二日間に、何度も立ち返る。その教訓は「LLMはVerilogが苦手だ」ではなかった。彼らは四半期ごとに良くなっている。その教訓は、ハードウェアでは、検証されているように見えることと検証されていることの隔たりが、八桁のマスクセットと六か月の遅れで測られる——ということだ。そしてこの空間へ殺到するツールは、その大半が「検証されているように見える」部分をより速くしようと競っている。
$10Mのマスクセットにおいて、非空虚な証明——あなたが管理するハードウェア上で走り、仕様の84ページを読んだ誰かが書いたアサーションに対してなされたもの——まで辿れない「証明済み」は、検証ではない。それは、見栄えのする体裁を伴った希望にすぎない。私たちがどうやってその違いを見分けるのかを見たければ、そのすべてが次に記されている——veriprajna.com/solutions/semiconductor-ai-verification。
チップは、レポートが何と言おうと気にしない。それは、シリコンが実際に作られたとおりのことしかしない。検証とは、その二つを同じものにする規律だ——そして、AIがそれらは同じだとミリ秒であなたに告げる瞬間こそ、まさにあなたが仕様に手を伸ばすべきときだ。
