驗證計畫、覆蓋率與獨立參考模型

驗證計畫把規格轉成可檢查的主張

不要只寫「運作良好」，而要列出重設後狀態、正常輸入輸出、暫停時保持、非法輸入處理與完成時點等具體主張。每項至少對應一個測試與觀察點，就容易找出遺漏條件。

為何需要獨立參考模型

若把移位 RTL 的切片^{i切片選取向量中一段連續的位元範圍。選取範圍決定結果的位寬與位元順序。 詳細內容}原樣複製為參考模型，索引錯誤也可能一起複製。改用整數乘法與 modulo，或字串尾碼比較等表示方式，有助於相互審查。但形式不同不會自動證明獨立性，仍要手算小案例確認。

覆蓋率不是通過次數

程式行被執行的 coverage，不等於功能情況已被檢查。reset×enable、state×input、full×push×pop 等交叉條件可能揭露錯誤。不要只靠隨機測試，應用定向測試補上少見但重要的組合。

N 個輸入的組合電路可窮舉 $2^N$ 組，但循序電路還有輸入時間序列。需分析所有狀態是否可達，以及不變量^{i不變量是在所有允許的執行過程中都必須成立的條件。例如，深度為 4 的 FIFO，其儲存數量必須一直介於 0 至 4。}是否在全部轉移中維持。有限次模擬通過紀錄，不能說成無限時間的數學證明。

由規格獨立產生答案，不要複製實作。發現失敗時，除實際值外，也記錄緊接之前的輸入與狀態。

縮小並記錄失敗

記下第一次 mismatch 的前狀態、輸入、預期值與實際值。刪除無關激勵，形成仍會失敗的最小反例後再修正。不只讓修改的測試通過，也要重新執行既有邊界與重設^{i重設將狀態回復至規格指定的初始值。必須一併定義它是同步或非同步，以及是否優先於其他控制訊號。 詳細內容}迴歸檢查。