Home

AIsimpV 研究導覽

AIsimpV 研究如何把 RTL 設計改寫成較小的抽象模型，並用獨立檢查的證書確認指定觀察行為包含原設計。這份 Wiki 是閱讀入口；實驗定義、程式碼和數據以 repo 文件 為準。

先看結論

• **可驗證性：**四個人工指定改寫（FSM、8/32-bit skidbuffer、32-bit pipeline）均通過證書檢查及指定 safety property；四個過粗抽象各有假反例，四份錯證書均被拒絕。完整報告
• **效能：**八輪配對量測沒有穩定的 property proof 加速；已知候選的轉換、證書和 property 驗證流程均比直接驗證原設計花更久。時間報告
• **較難的 FIFO：**三個原生 memory 配置有可驗證候選，但總成本沒有大幅下降；部分候選只是把原 property proof 移到 certificate。搜尋報告
• **自由改寫：**axilxbar 和 PicoRV32 候選展示了設計縮小的構想，也展示了刪掉交易、狀態或 checker 的風險；目前沒有證據把這些候選稱為原設計的正確抽象。axilxbar · PicoRV32
• **PicoRV32 多數任務：**候選 05 用 JasperGold 在 86 題中有 72 題 bounded assertion pass；8 題 M、6 題 CSR 有反例。這跨過 69 題的數字門檻，但不是行為包含或等價證明。逐題結果

怎麼讀

1. 結果與證據：逐項查看做了什麼、得到什麼，以及哪些結論尚不成立。
2. 驗證方法與重跑：理解 certificate、property proof、replay 的分工，以及如何在本機重跑。
3. 需要確切 task、hash、原始數據或失敗紀錄時，從上述頁面進入 repo 的正式報告和資料檔。

早期的 feasibility sprint 與 9/23 執行計畫保留原本的時間和範圍；閱讀當前結果請優先看已執行報告。