ASICパズルの結果

ASICパズルの結果 2026年10月2日 | 13分で読む Facebookで共有 Twitterで共有 LinkedInで共有 投稿者: Benjamin Devlin 投稿者: Anish Singhani 8月に、私たちは小さなチップの最終GDSレイアウトを提示し、それが何をするかを解明するように求めるパズルを公開しました。物理的なレイアウトは提供しましたが、ネットリストや内部信号名は提供せず、内部をリバースエンジニアリングするのは参加者の皆さん次第でした。この記事では、チップが何をするのか、そして皆さんがどのように解決したのかを、お気に入りの提出物の一部に言及しながら探求します。 応募作品 米国、インド、英国、オーストラリアからの応募が大部分を占め、30カ国以上から約400件の応募がありました。参加者には、高校生、研究者、現役エンジニア、退職者などが含まれていました。ほとんどの solvers は、KLayout、Yosys、Z3 と、Python、Rust、C++、OCaml、Haskell、さらには Odin で実装されたカスタムツール（多くはAIで書かれたもの）を使用しました。 解決策 多くの皆さんが発見したように、このチップは11x11のスターバトルパズル、別名「ツー・ノット・タッチ」のハードウェアチェッカーです。目標は、各行、各列、および各色の領域に正確に2つの星を配置することです。2つの星は、対角線上であっても触れ合うことはできません！チップは121サイクルの入力を受け付け、各入力は対応するマスに星を配置するかどうかを示します。その後、これらの入力に対して複数の並列チェックを実行します。 各行および各列に対応する2ビットカウンタ。各行/列に正確に2つの星が必要であることを要求します。 マスを領域にマッピングする121ビットROMと、各領域に対応する2ビットカウンタ。各領域に正確に2つの星が必要であることを要求します。 2つの星が対角線上であっても決して触れ合わないように追跡するための遅延線。 特定のイースターエッグ出力を生成するために使用される、星の総数をカウントするカウンタ。 パズルのチェックは、成功信号を生成するためにすべてANDされます。出力ジェネレータは、ROMに文字列を格納します。解決策がプレーンテキストで表示されるのを防ぐため、ゲームボードに基づいた小さなLFSRによって難読化されています（ただし、LFSRを攻撃するのを止めることはできませんでした！）。成功が達成されると、出力ロジックは解決策文字列を難読化して出力します！(* TWO STARS *)ほとんどの不正解は「TRY AGAIN」という文字列を出力しますが、いくつかはこの下にリストされているイースターエッグをトリガーしました。パズルチップは、SKY130オープンソース標準セルライブラリを使用して、LibreLaneツールチェーンで設計されました。 どのように解決したか 以下では、パズルの解決に関わるステップを、お気に入りのいくつかの writeup からの例とともに説明します。 レイアウトからのネットリスト抽出 最初のステップは、GDSレイアウトからゲートレベルのネットリストを抽出することでした。開始を容易にするために、GDSファイルにセル名（sky130_fd_sc_hd__nand2_2など）を残しておいたため、MagicやKLayoutなどのツールでLVS1パスを使用して生のゲートレベルネットリストを抽出できました。しかし、一部の参加者は、独自のネットリスト抽出ツールを作成するという追加の課題に取り組みました。Vladislav Shapovalovの writeup は、C++で独自の抽出パイプラインを記述し、GDSを解析して各セルの形状を抽出し、セル名と組み合わせて完全な論理ネットリストを生成した方法を示しています。その後、メインのパズルGDSで使用する前に、ウォームアップデザインで試行錯誤してパイプラインをデバッグしました。（Vladislav Shapovalovの writeup の図1よりトリミング） ネットリストのシミュレーション ネットリストを復旧すると回路グラフが得られますが、それをシミュレートするには各セルの動作を知る必要もあります。一部の参加者はVerilogを生成し、SKY130セルモデルと既存のシミュレータを使用しました。Stephen Ebertのような他の参加者は、独自の評価器を構築し、レジスタ間のロジックを計算し、各クロックエッジでレジスタを更新しました。提供された波形は、入力シーケンスを再生し、比較する期待される出力を与えました。同じシミュレータを使用して、候補ボードをテストし、出力ジェネレータを実行して回答を読むことができました。しかし、その波形に一致したからといって、シミュレータが正しいとは限りませんでした。Alejandro Soto Francoは、すべてのタイハイセルを間違って評価したにもかかわらず、提供されたトレースを再現したPythonモデルを説明しています。これらのセルは定数1を供給すべきですが、モデルはそれらを評価せず、出力はゼロのままでした。この間違いにより、隣接チェックが無効になりました。そのモデルを使用した参加者は、星が触れ合っているように見える有効なボードを見つけることができました。Alejandroは、追加の入力に対して別のIcarus Verilogシミュレーションと比較することで、この問題を発見しました。 ロジックのトレース 一般的なアプローチであり、私たちが最も期待していたのは、「成功」出力から始めて、ネットリストを逆にたどって、有効な入力の条件を特定することでした。フロアプランにいくつかのヒントを残しておきました。レイアウトの各「島」は、元のRTLデザインの単一のモジュールに対応していました。Sanjay Ravishankarはこれを最大限に活用し、各領域の上に境界ボックスを描き、回路図をこれらの境界ボックスに分割しました。彼は彼の writeup にその素晴らしい視覚化をいくつか含んでいます。モジュール間の接続を見てモジュール境界を確認した後、各モジュールをシミュレートしてその機能と全体像における位置を理解しました。Sanjay Ravishankarの注釈付きレイアウト。論理の島が機能別にラベル付けされています。彼の writeup からの図。 動的探索 別のアプローチは、異なる入力でチップをシミュレートし、ロジック関数自体をあまり気にせずに、中間信号がどのように変化するかを観察することでした。Aaron Shiは、信号とシステムクラスで学んだことを活用し、「ネットリストをシステムとして扱い、さまざまな位置でインパルスを当てました…その後、すべてのフロップをゼロベースラインと比較しました。変化するフロップはその1ビットへの応答です」と彼の writeup に書いています。彼はその後、フロップが行、列、領域に対応していることに気づき、それぞれが成功するために正確に2に累積する必要があることに言及しました。そこから、成功に必要な条件を満たすソリューショングリッドを構築しました。Aaron Shiのシミュレータ。レジスタは、最初に高くなったサイクルで色分けされています。このすべてが1になる実行は、行カウントと隣接チェックをトリップします。彼の writeup からの画像。 SATソルバー 私たちが見たもう一つのアプローチは、回路が何をするのかを知る必要なしに、SATソルバーを使用して正しい解を見つけることでした。ある意味で、SATソルバーはこの種の課題に最適です。固定数のクロックサイクルでエンコードされた回路を受け取り、特定の条件（この場合は成功出力）を真にするために必要な入力を計算できます。このようなツールは、ハードウェア検証でも頻繁に使用されます。SATソルバーを使用して、チップが望ましくない出力動作を持つ入力のセットが存在するかどうかを証明します。しかし、このような課題にSATソルバーを使用する欠点は、回路の内部動作についてはあまり明らかにならず、望ましい出力状態に到達するために必要な入力だけがわかることです。しかし、Lokesh Aravapalliは両方の世界の最良を見つけました。彼はSATソルバーを使用して有効な入力セットを取得することから始めましたが、その後、これらの入力を使用して実際に回路の目的を分析して理解し、回路のクールな視覚化を構築しました！ 出力ジェネレータのクラッキング このようなパズルでは、私たちが書いている間には考慮しなかった解決方法を見つける人々がいるため、常に予期しない解決策と非定型な思考があります！一部の人々が試みたことの1つは、出力モジュールから直接解決策文字列を抽出することでした。チップには、LFSRによるボードの「チェックサム」を計算するという基本的な難読化が含まれており、それがROMに格納される前に解決策文字列とXORされていました（これにより、回路を単純に編集して「成功」入力を出力ジェネレータに駆動しても、スクランブルされた出力が生成されました）。しかし、Gabriel Taboadaはこれがどのように機能するのかに興味を持ち、出力回路をリバースエンジニアリングして、正確にどのように機能するかを理解しました。