结合记分板与局部不变量

以输入接收为验证基准

记分板根据每个已接收输入计算预期结果，并将其入队。输出交付时，与最旧的预期数据项比较。直接从约定计算，而不是照搬每个流水线寄存器，有助于减少共同错误。只有输入握手时才添加条目；呈现但被拒绝的输入不属于未完成工作。

对于已接收的 ADD 输入 tag10:(250,10) 和 tag11:(3,5)，预期为 [(10,4,carry1),(11,8,carry0)]。有效但停顿的输出不会移除条目。交付 tag10 只移除该条目。重复 tag10，或数值 8 却标为 12，都是错误，即使部分数值匹配。应包括所有相关标志和伴随字段。

局部不变量能找出第一个失败时钟沿，而不是只发现最终不匹配。内部占用量为 FIFO count 加各级有效位。允许复位或清空时，应加入取消计数，并在两个监视器中使用相同的时钟沿策略。

结合数值边界与时序情况：零、最大值、进位和借位、连续流量、气泡、长停顿、满状态替换和最终排空。记录随机种子，使失败可复现。可行时穷举小型控制空间。

完成检查需要进展假设和超时。一旦接收端持续 ready，未完成工作就应排空。无限停顿时，应要求数据保持和有界占用量。有意破坏进位或标签延迟应使检查失败；这种变异测试衡量测试敏感度。通过 Node 模型不能验证 HDL 布线、X/Z 行为、跨时钟域或实现时序。只报告实际观察到的执行范围。