驗證方法與重跑

證明鏈

1. 凍結原設計 C、抽象 A 與 同一份 contract。改了 property 或環境條件，就變成另一個問題。
2. checker 驗證證書中的狀態映射 h、不變量 J 和自由輸入 witness w，確認 C 的每個合法步驟能匹配 A，且觀察值相同。拒絕或 timeout 不算設計 bug。
3. property backend 獨立證明 A 的指定 safety property；它不讀取 h/J/w。只有證書通過且 A 的 property 為 SAFE，才能把該 property 推回 C。有限深度 BMC 通過只算 BOUNDED。
4. A 若有反例，依相同初值、公共輸入與觀察序列在 C 做 exact replay；無法重播的反例是 SPURIOUS_TRACE，不是原設計 bug。

詳細定義見 public-task semantics v1、原始 v0；RTL frontend 的支援範圍見 frontend decision。四題公開 pilot 採單一正緣 clock、更新前取樣、有限 bit-vector 狀態；同步 reset 是自由的公共輸入。舊 frontend 不支援任意 memory、未知初值或多 clock，遇到界線會拒絕。

原生 memory FIFO 搜尋另用 獨立 protocol 和 synchronous-product adapter，保留上游 assertions 與部分未初始化 memory；它不表示舊 finite-BV frontend 已支援 memory。

PicoRV32 上游 assertion 重跑

這組 RTL/SVA checker 優先用本機 JasperGold 直接執行，不需要 Yosys 或 Boolector。將 pinned riscv-formal c992aa61fdfe0846c5ed90324c596202a1c69b76 產生的 86 個 .sby task 指向 --checks；腳本取出相同 defines/checker，並以 Jasper 原生 assume -constant 保留上游 rand_const 的固定選擇值。每題依原設定的檢查拍數做 bounded proof；PASS 不是無界證明或行為包含。完整命令、結果與限制。

本機重跑核心實驗

需要 Python 3.11+、PATH 上的 Z3 CLI，以及 uv。在 repo 根目錄執行：

sh scripts/bootstrap_yosys.sh
python3 -m unittest discover -s tests -v
python3 -m rtl_relate demo --out results/my-first-run
python3 -m rtl_relate.wednesday --out results/my-wednesday-run

每次使用新的輸出目錄。demo 會保留 queries、solver 輸出、模型、證書、RTL 複本和時間；summary.json 與 results.csv 可檢查結果矩陣。更多選項、單獨重驗證書及目前模型 API 設定見 README 的 Reproduce。時間量測和原生 memory 搜尋有各自的命令、固定版本、成本定義和證據索引。

查看結果時先確認 task／contract、ACCEPTED／SAFE／BOUNDED／UNKNOWN／UNSUPPORTED 的區別，再看候選與原設計的實際差異；frontend PASS 只證明指定工具可處理輸入，不能代替 property 或行為包含的證明。