計分板與不變條件

區分兩種參考

以直接數學參考，使用獨立 i/j/k 迴圈計算寬位元總和。另用獨立時序模型，讓 A 向右、B 向下移動。將 RTL 索引輔助函式複製至黃金模型，可能重現相同錯誤。先從固定手算範例開始，再擴展至可重現的隨機輸入。

結果計分板以 job 與全域輸出座標為鍵。比較各接收值，並將鍵標為已接收。重複鍵表示重複，非預期鍵表示位址錯誤，未接收的預期鍵表示遺漏。零結果仍須交付。填補的超範圍座標絕不得寫入。

檢查陣列內不變條件

各 PE 必須恰好消費 [0,1,...,K−1]。相配的有效運算元需要相同 job 與 k 標籤。Count 保持於零到 K。暫停邊緣保持運算元、valid、標籤、累加器與 count。Clear 後 count 與累加器為零，且沒有有效權杖。阻塞結果在 valid 持續成立時保持 data 與 job。

2×2 範例中，最後 PE 在 E2 之後為十八，E3 之後為五十。E2 的全域 done 錯誤應同時使數值與時序檢查失敗。反之，重複與遺漏相同值的乘積可能保留最終總和；項目追蹤能抓出這種巧合。

儲存隨機種子、矩陣、維度、位元寬度與暫停位置。記錄第一個不符的 PE、項目與實體邊緣。刻意標籤錯誤應明顯失敗，而非悄悄消失。

一致地觀察 E_t 之後狀態。Node 參考執行、RTL 編譯、RTL 模擬、合成、時序收斂、DDS 專案執行與開發板測試，各自證明不同事實。提供的 Node 程式驗證算術與排程模型。未來 RTL 測試可重用測試資料，但必須保留自己的工具版本、命令與紀錄。