Results and Evidence

結果與證據

以下按驗證強度整理，避免把不同實驗的 frontend PASS、property SAFE、證書通過或執行時間混成同一個成功率。完整紀錄在各報告及其連結的資料檔。

實驗	已觀察到的結果	解讀界線	詳細資料
四個人工 RTL 改寫	FSM、skid8、skid32、pipeline32 均為 certificate ACCEPTED、property SAFE；四個 coarse 候選的 abstract CEX 無法在原設計重播，四份錯證書被拒絕	四個 task 來自三個設計家族，其中兩個 skidbuffer 位寬屬同一家族；這些小案例證明可行性	9/23 報告 · 逐列 CSV
LLM 固定 pair 與 joint skid8 pilots	固定 pair 與新生成的 18→10-bit RTL 抽象都出現獨立驗證通過的候選；失敗的 API／截斷／hash attempts 另計	單一 skidbuffer 家族的成功樣本；不代表新抽象方法或驗證加速	直接 API 結果 · 早期人工／Codex 結果
八輪配對時間	五個已知候選中，只有 FSM 的 abstract property 中位數略低於 concrete；pipeline 為 C 0.618 秒、A 1.070 秒；五條候選驗收流程都比直接 concrete proof 慢	property、solver 程序、certificate／轉換成本分開計；沒有穩定加速結論	時間報告 · 逐輪 JSON
原生 memory FIFO 搜尋	三個配置的 stateless 候選總驗證時間 18.0／23.7／34.6 秒，對照原設計 19.6／28.8／31.7 秒；另一個 21-bit stateful 候選需 36.9 秒	三個配置都屬同一 FIFO 家族；快速 abstract proof 可把工作轉移到 certificate，沒有大幅端到端加速	搜尋報告 · 數據 JSON
上游 axilxbar 三次自由改寫	有 property 改寫、固定優先權 grant、read-focused state model；三份候選都通過指定的 frontend 檢查	沒有執行 BMC、prove 或行為包含；其中一份刪除原 checker，另一份把 AXI 輸出固定為零	報告 · 候選對照
PicoRV32 上游 ADD property	DeepSeek 02 固定回報零值後約 1 秒 BMC PASS；Sonnet 5.5 保留完整資料路徑，BMC 約 10 分 29 秒仍無結論；Opus 5.5 medium 在新增單一 assertion 指示後，產生 370 行 partial 主核心，原 checker 約 2.41 秒 PASS，並在第 20 拍 cover 非零 5 + 7 = 12	Opus 刪除 compressed、記憶體、分支、M/CSR 等合法前序路徑且改變退休時序；這是受限模型自己的性質，沒有與原核的 refinement 證明，也不能把時間當成同一義務的加速比；模型、effort、提示詞均不同	報告 · Opus 評估
PicoRV32 多數 assertion 任務	JasperGold 直接驗證原版 86/86、候選 05 72/86 題 bounded pass；候選 8 題 M 和 6 題 CSR 有反例；62 題通過的非 M 指令 checker 之非 trap cover 可達	72/86 超過 69 題門檻，但只是固定拍數的 task pass；沒有行為包含證書，task 也非獨立行為樣本	方法與結果 · 逐題 JSON

其他仍有用途的紀錄

• 約十秒級 baseline 篩選：64×32 與 256×32 FIFO 的直接 proof 三次中位數為 5.772／7.313 秒；當時尚未做抽象和證書。後續原生 memory 搜尋採用不同配置與方法，數字不可直接拼接。
• finite FIFO 4×8 接入：舊 finite-BV frontend 對未定義值分支與匿名 BTOR input 回報 UNSUPPORTED；沒有把它算進四題成功矩陣。
• 衍生 property 的 axilxbar 流程試跑：與上游 assertions 的三次實驗分開。第一份候選只有 frontend／property 接線 PASS，未執行 BMC、prove 或包含檢查。

實驗的原始 prompt、工具輸出及部分大型 evidence 留在本機或 release；Git 追蹤的報告會標明哪些資料公開、哪些需要本機重跑。