STEP 1430 — D-FUMT₈ 汎用等価性検査器 (10 operator PASS)

2026-08-27 · STEP 1426 feasibility の正式 tool 化 · 10/10 PASS 26 秒 · eqy + sby + bitwuzla

⚠ 命名 confusion 予防 (STEP 1446 retrofit): 別 tool の STEP 1429 「D-FUMT₈ 関数完全性検査器」と命名近似だが 完全別 layer + 別 concept — 前者 = MCP tool、演算子集合の functional completeness 判定 / 本 tool (STEP 1430) = Verilog RTL、 2 実装の semantic equivalence 判定。詳細対比 → docs/CROSS_REFERENCE_STEP1429_1430.md

要約

STEP 1426 で実測した「3-bit 全単射で eqy 薄い wrapper OK」の藤本さん見立てを **正式な汎用 8 値 equivalence checker tool** に昇格。 D-FUMT₈ ALU の 10 operator (NOP/AND/OR/NOT/OMEGA/PHI/PSI/XOR/ADIABATIC/RESET) それぞれで gold vs alt 実装の意味等価性を bitwuzla SMT depth 1 exhaustive で verify、 **10/10 PASS 26 秒**。

実測 result

✅ 10/10 PASS in 26 秒

=== D-FUMT₈ equivalence check (10 operators) ===
  OSS_ROOT: /c/oss-cad-suite-parent/oss-cad-suite
  OP_DIR:   /c/Users/user/rei-aios/data/verilog/operators
  WORK_DIR: /c/Users/user/rei-aios/data/verilog/operators/_work

  [PASS] nop
  [PASS] and
  [PASS] or
  [PASS] not
  [PASS] omega
  [PASS] phi
  [PASS] psi
  [PASS] xor
  [PASS] adiabatic
  [PASS] reset

=== Summary ===
  PASS: 10 / 10
  FAIL: 0
  SKIP: 0
  Elapsed: 26s

Operator matrix (10 件)

#	op	arity	gold	alt	意味
1	NOP	u	8-entry ternary chain	`out = a`	identity
2	AND	b	32-entry casex + cross-tier if-else	flat 64-entry case	Belnap meet + higher-tier + LOW-wins
3	OR	b	32-entry casex + cross-tier if-else	flat 64-entry case	Belnap join + higher-tier + LOW-wins
4	NOT	u	8-entry ternary chain	bit-algebra (`flip_lower ∨ flip_zero_inf`)	classical-axis flip
5	OMEGA	u	8-entry ternary chain	`{a[2], a[1], a[0] & ~a[2]}`	idempotent collapse
6	PHI	u	8-entry ternary chain	`a ^ 3'b001`	pair-swap
7	PSI	u	8-entry ternary chain	`{1'b0, a[1:0]}`	convergence (clear bit2)
8	XOR	b	64-entry ternary chain	`a ^ b`	bit-parallel XOR
9	ADIABATIC	u	`(a==SELF) ? SELF : a`	`out = a`	SELF-recover (tautologically identity)
10	RESET	u	8-entry ternary chain (all 000)	`3'b000`	force FALSE

Quick start

# 前提: OSS CAD Suite installed (STEP 1426 で install 済 = C:/oss-cad-suite-parent/oss-cad-suite/)

# Single operator
bash scripts/eqy-dfumt8-check.sh not

# All 10 operators
bash scripts/eqy-dfumt8-check.sh all

実装 discipline 発見

1. `case` + `output reg` は $mem_v2 → xprop 通らない

初回 run で 6/10 が sby ERROR (Unhandled cell $mem_v2)。 Yosys が case-with-full-input-coverage を ROM primitive 化、 eqy 内部の xprop -formal pass が $mem_v2 対応外。

解決: gold を output wire + assign ... = (a==...) ? ... : ... chain 化で統一。全 10 operator で assign form 統一 → 26 秒で 10/10 PASS。

2. eqy strategy = `sby` 選択

sat strategy は output reg 系 skip、 sby 経由で SMT backend fallback = 汎用性高。

3. file format 規約: `ifdef GOLD/ALT split

各 operator の .v file 1 つに 2 実装を preprocessor で埋め込み、 script が awk で抽出。 file 数半減 + 対応 pair の明示。

Honest scope (7 条)

10 operator の「gold vs alt」 equivalence proof のみ — 「回路 A vs 実際 synthesize 後 gate netlist」は未対応 (別 STEP candidate B.1)
8 値 = 2³ 全単射 encoding 前提、 5/7/9 値の場合 well-formedness constraint 必要
gold impl 全て assign chain 統一 — 元 dfumt8_alu.v (case 形式) は保持だが、 equivalence check target は chain 版 ($mem_v2 回避)、元 code の直接 verify は STEP 1426 sby 6-property BMC で cover
make workaround — OSS CAD Suite Windows bundle に make 未同梱、 script 内 eqy -m + sby 手動 2 段で自動化
SMT backend = bitwuzla (SBY default)、 depth 1 exhaustive で全 input space (unary 2^3=8 or binary 2^6=64)
spec 定義 fault は検出しない — gold と alt が同じ齟齬なら PASS、 spec 検証は Lean 4 refinement + SymbiYosys property assertion で別途 cover
novelty ゼロ — OSS CAD Suite 標準 workflow を D-FUMT₈ に適用しただけ、「世界初 8 値 equivalence checker」主張なし

拡張 candidate (未来 STEP)

B.1: 元 dfumt8_alu.v (case 形式) 自体を gold として synth 後 gate netlist と比較
B.2: 他 3-bit 対称回路 (Cl(3,0), quaternion 等) の等価性 verify
B.3: 8×8 binary op の交換律 (op(a,b) == op(b,a)) property を eqy と併用
C: make 導入で eqy -f 単発 invoke 化 (CI ready)
D: GitHub Actions で PR ごと自動 verify

Artifact (STEP 1430)

scripts/eqy-dfumt8-check.sh — runner script (~150 行、全 op 一括 or 単発)
data/verilog/operators/dfumt8_*.v × 10 — gold + alt implementations
data/verilog/operators/_work/ — sby workdir (gitignored)
data/verilog/EQUIVALENCE_CHECKER.md — tool doc
data/verilog/STEP1426_REPORT.md — feasibility 起点 report

Rei stack alignment

STEP 1426 — feasibility 起点 (OSS CAD Suite install + 藤本さん 3 見立て verify)
STEP 1006 — Verilog RTL R-1 (dfumt8_alu.v 起源)
STEP 1029 — Tang Console 138K 物理 silicon
STEP 1030 — Aer + Heron 4-substrate (empirical fidelity 0.954、別 evidence)
STEP 1397 — d8_verify (実装ドリフト検出、汎用 equivalence checker とは別 tool)
Paper 145 v0.6+ — SymbiYosys wrapper (Property 6 spec bug 検出 → 次 arc B)

要約