結合計分板與局部不變條件

以輸入接受為驗證基準

計分板由每筆被接受輸入計算預期結果，並排入佇列。輸出交付時，比較最早的預期項目。直接依契約計算，而非逐一模仿所有管線暫存器，可減少共同錯誤。只有輸入交握才新增項目；呈現卻被拒絕的輸入，不算尚未完成工作。

接受 ADD 輸入 tag10:(250,10) 與 tag11:(3,5) 後，預期 [(10,4,carry1),(11,8,carry0)]。有效但停頓的輸出不會移除項目。交付 tag10 只移除該項。即使部分數字相符，重複 tag10 或將數值 8 標為 12 都是錯誤。納入所有相關旗標與伴隨欄位。

局部不變條件找出第一個失敗邊緣，而非只看最終不符。內部占用量是 FIFO count 加上各級 valid 位元。允許重設或 flush 時，加入取消計數，兩種監控都使用相同邊緣策略。

將數值邊界與時序情況結合：零、最大值、進位與借位、連續流量、空泡、長停頓、滿時替換與最終排空。記錄隨機種子以重現失敗。可行時窮舉小型控制空間。

完成檢查需要進展假設與逾時。接收端持續 ready 後，尚未完成工作應排空。無限停頓下，則要求保留與有界占用量。刻意破壞進位或標籤延遲，應使檢查失敗；此變異測試衡量敏感度。Node 模型通過，不驗證 HDL 接線、X/Z 行為、跨時脈域或實作時序。只回報實際觀察的執行範圍。