记分板与不变量

分开建立两种参考

使用直接数学参考，通过独立的 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 全局完成的错误应同时导致数值和时序检查失败。反过来，重复和遗漏相等乘积可能使最终和不变；项跟踪能发现这种巧合。

保存随机种子、矩阵、维度、位宽和暂停位置。记录第一个不匹配的 PE、项和实际时钟沿。刻意制造的标签错误应明确失败，不能悄悄消失。

始终一致地在 E_t 之后观察状态。Node 参考执行、RTL 编译、RTL 仿真、综合、时序收敛、DDS 项目执行和板级测试分别证明不同事实。提供的 Node 程序验证算术和调度模型。未来 RTL 测试可复用测试数据，但必须保留自己的工具版本、命令和日志。