# rei-fpga 設計仕様書 v0.1 回路化パイプラインの出力を FPGA に落とし、**元の設計と等価であることを機械証明する**層。 Claude Code に追加実装を投げる際はこの文書を基準にすること。 --- ## 0. この配線が閉じるもの ``` 回路化パイプライン ──> 論理回路を生成する （生成） │ FPGA ──────────────> その回路を実体化する （実装） │ rei-solver ────────> 実体が仕様と一致することを証明する （証明） circuit_equivalence ``` 3 つが**同一の IR** を共有することで輪が閉じる。形式を 1 つに統一することが唯一の条件で、 それ以外の工夫はすべて後回しでよい。 --- ## 1. 何を証明し、何を証明しないか **ここを取り違えると、この層は害になる。** | 段 | 比較対象 | 証明すること | |---|---|---| | `spec` | 参照仕様 × 設計 | **設計が正しい** | | `generic` | 設計 × 汎用合成後 | 合成器が論理を変えていない | | `gowin` | 設計 × LUT マッピング後 | LUT に詰めても同じ | `generic` と `gowin` が証明するのは「**道具が回路を変えなかった**」ことだけである。 **「回路が正しい」ことは証明していない。** 壊れた設計を合成すれば、 壊れたまま忠実に実装され、両段とも proof で通る。実測で確認済み （`test_synthesis_faithfully_implements_a_broken_design`）。 設計そのものの正しさを見るには、独立に書いた参照仕様を渡すこと。 ```bash python -m rei_fpga.cli prove design.json --spec reference.json ``` 参照仕様は**設計とは別の経路で書かれていなければ意味がない**。 同じ生成器の出力を両方に渡すのは、自分の答案を自分で採点する行為にあたる。 --- ## 2. 中間表現 (IR) rei-solver の `circuit_equivalence` が受け取る形式と**同一**。 ```json { "name": "adder4", "inputs": ["a0", "a1", "b0", "b1", "cin"], "gates": [ {"op": "xor", "out": "_x1", "args": ["a0", "b0"]}, {"op": "and", "out": "_a1", "args": ["a0", "b0"]} ], "outputs": ["s0", "cout"] } ``` ゲート種: `and or not xor nand nor xnor buf const0 const1` （増やす場合は `rei_solver/engines/z3_engine.py` の `_GATES` も同時に。） ### 不変条件 - `gates` はトポロジカル順序（参照は必ず既出の信号） - 1 つの信号を 2 回駆動しない - `outputs` は必ず駆動されている 3 つ目が特に重要で、未駆動の出力を黙って通すと**証明が空虚に真になる**。 `Circuit.validate()` が実行前に弾く。`topo_sorted()` は順序を直しつつ 組合せループを検出する。 --- ## 3. 合成フロー `yowasp-yosys`（WASM 版 yosys、pip で入り追加依存なし）を使う。 システムに実 yosys があればそちらを優先する。 ``` generic: read_verilog → synth -top X → abc -g AND,NAND,OR,NOR,XOR,XNOR,ANDNOT,ORNOT → opt_clean → write_json gowin: read_verilog → synth_gowin -top X -json ``` Verilog エミッタは意図的に素朴で、1 ゲート 1 `assign` の逐語訳に徹する。 ここで最適化すると「エミッタのバグ」と「合成器のバグ」の区別がつかなくなる。 --- ## 4. ネットリスト逆変換 配線の要。合成後を IR に戻せて初めて機械的に突き合わせられる。 ### 対応セル | 種別 | セル | |---|---| | yosys 内部 | `$_AND_ $_OR_ $_NOT_ $_XOR_ $_NAND_ $_NOR_ $_XNOR_ $_BUF_` | | 同・複合 | `$_ANDNOT_ $_ORNOT_ $_MUX_ $_NMUX_ $_AOI3_ $_OAI3_ $_AOI4_ $_OAI4_` | | GOWIN | `LUT1〜LUT4`, `MUX2_LUT5/6/7/8`, `IBUF`, `OBUF`, `VCC`, `GND` | ### LUT の展開 GOWIN の LUT は `INIT`（真理値表そのもの）を持つ。これを最小項の和に展開して 基本ゲートに落とす。証明器を一切変更せずに済むよう、疎結合を優先した。 `INIT` は MSB 先頭のビット列文字列で、添字 `i` のビットは `int(INIT, 2) >> i & 1`（実測で確認）。全 0 なら `const0`、全 1 なら `const1`。 ### 明示的に落とすもの - **未知のセル** — 黙って無視すると証明が空虚に真になるため中断 - **順序回路**（DFF/latch）— 組合せ等価性検証の対象外。BMC が必要 - **未定義値 (x/z) を運ぶネット** — 同上 セルの追加は `netlist.py` の分岐に 1 つ足すだけでよい。 **ただし、追加したら必ず `TestTeeth` に破壊試験を足すこと**（§6）。 --- ## 5. 判定 | verdict | 意味 | 終了コード | |---|---|---| | `proved` | 全段が `assurance="proof"` | 0 | | `refuted` | いずれかで反例が出た | 1 | | `inconclusive` | エラー、打ち切り、判定不能 | 2 | `refuted` のとき `counterexample_input` に**具体的な入力ベクタ**が入る。 これは推測ではなく、独立に評価すれば誰でも再現できる証拠である。 `inconclusive` は「等しい」でも「等しくない」でもない。ここを `proved` 寄りに 解釈してはならない。 --- ## 6. 検証器に歯があることの確認 **この項目が最重要。** 検証器が壊れた実装を弾けなければ、 すべての `PROVED` は空虚に真である可能性がある。 `TestTeeth` が実際に行うこと: 1. `adder4` を GOWIN 合成して LUT ネットリストを得る 2. LUT の `INIT` を**1 ビットだけ反転**する 3. 逆変換して等価性検証にかける 4. **反例が返ること**を確認する 5. 返された反例入力を、証明器から独立した素朴な評価器で再計算し、 本当に出力が食い違うことを確認する 5 が肝で、証明器の言い分を鵜呑みにせず第二の実装で照合している。 新しいセルや最適化を追加したら、必ずこの破壊試験を拡張すること。 --- ## 7. 実機ビルド（Tang Console 138K） ### ピン番号について `boards.py` に実ピン番号は**入れていない**。推測で書いた番号は合成も 配置配線も通ってしまい、実機で初めて誤りに気づく類の間違いになる。 しかも**証明器はピン割当を検証しない**。ここだけは人間が公式資料と 突き合わせる必要がある。 ```python from rei_fpga.boards import TANG_CONSOLE_138K, make_cst board = TANG_CONSOLE_138K.with_pins({"a": "", "b": "", "y": ""}) open("design.cst", "w").write(make_cst(circuit, board)) ``` ### 手順 1. `rei-fpga prove design.json` で `PROVED` を確認（先にやる） 2. `rei-fpga verilog design.json -o design.v` 3. `rei-fpga cst design.json --pins pins.json -o design.cst` 4. GOWIN EDA で `design.v` + `design.cst` を読み、配置配線してビットストリーム生成 5. Tang Console に書き込み 証明を通してから実機に行くこと。順序を逆にすると、実機で出た不具合が 論理の誤りなのか配線の誤りなのか切り分けられなくなる。 ### 現状の限界 GOWIN の配置配線（`nextpnr-himbaechel` または GOWIN IDE）は本パッケージに 含まれていない。ビットストリーム生成後の**最終ネットリストに対する 等価性検証は未実装**である。商用 LEC が押さえている領域であり、 やるなら `nextpnr` の出力を読む経路を足すことになる。 --- ## 8. 拡張の順序 1. **参照仕様の自動生成** — 回路化パイプラインとは独立な経路で spec を作る。 ここが埋まらない限り「設計が正しい」は人間が保証していることになる 2. **順序回路対応** — DFF を含む回路の BMC（rei-solver 側に `bmc` op を追加） 3. **配置配線後の検証** — `nextpnr` 出力の読み込み 4. **規模の拡大** — 現在は総当たり相当を Z3 が処理している。 数万ゲートに乗せるなら構造ハッシュと切り出し (partitioning) が要る --- ## 9. 検証済みの事実（実測） | 項目 | 結果 | |---|---| | 統合テスト | 26/26 通過 | | `xor_nand` / `adder4` / `priority8` の generic 段 | すべて proof | | 同・gowin 段（LUT マッピング後） | すべて proof | | GOWIN 合成が実際に LUT を出していること | LUT1〜4 / MUX2_LUT5〜8 を確認 | | LUT `INIT` 1 ビット反転（4 箇所） | すべて反例を検出 | | 反例入力の独立再評価 | 出力の食い違いを確認 | | 壊れた設計 × 参照仕様 | 反例つきで refuted | | 壊れた設計 × 自身の合成結果 | proved（道具は忠実、設計は誤り） | | 未知セル・順序回路・未定義値 | すべて明示的に中断 | | 未割当ピンでの `.cst` 生成 | strict モードで拒否 |