计数器调试与最小反例

最终值正确，顺序仍可能错误

计数器最终为 0，并不能证明 reset 和回绕正确。一直停在 0 的电路也会产生相同结果。需要设置分别揭示正常递增、保持、复位^{i复位 将状态恢复为规定初值的控制。必须同时规定其同步或异步性质，以及相对于其他控制的优先级。了解更多}和边界回绕的观察点。

刻意让两个功能发生冲突

若只分别测试各个控制，优先级错误很难被发现。

每列记录一个上升沿^{i上升沿 时钟从 0 变为 1 的瞬间。它不同于表示整个 CLK=1 区间的电平。了解更多}的观察结果。输入取自边沿前，名称带 after 的状态取自更新后。列的排列表示采样顺序，并非描绘物理传播延迟^{i传播延迟 从输入变化到输出稳定为正确值所需的时间。逻辑表达式等价与时间特性是两回事。了解更多}。初始 count=5。错误电路只在 enable 内检查 reset，因此第一边沿仍保持 5。即使最终值相同，首次不匹配也会暴露缺陷。

模 8 参考电路从初始 101 开始。选择 enable=0、reset=1，再推进时钟。正确值应为 000；将 reset 放在 enable 内的错误 RTL 会保持 101。释放 reset 后，再区分 enable=0 的保持与 enable=1 的递增。

用参考模型寻找首次不匹配

此表达式是以正常状态 0~M-1 为前提的功能模型。越界状态恢复应作为独立策略加入。每个边沿都计算预期值并与实际值比较。首次不匹配之前那个边沿的输入与状态，是寻找原因的最小起点。

若失败在一千个周期后才出现，尝试删除无关输入区间，用三到五个边沿重现同一错误。修复 RTL 后，将这一最小反例保留为回归测试。应分别审查修改后的规格与代码，避免把设计和测试同时改成同一个错误条件。