18 / 37 · 测验

设计检查：位宽、优先级与回绕边界

依据给定的状态转移规格，判断边界值与同时到达的控制输入。

模 10 计数器的约定

对于四位 unsigned^{unsigned 将位串解释为非负整数的规则。n 位范围为 0 到 2^n−1，可能与同一位串的 signed 解释不同。了解更多} count，优先级依次为 reset、enable、hold。reset=1 时归零；否则 enable=1 时，若 count 不小于 9 就归零，其余状态递增 1。

N=\lceil\log_2 10\rceil=4

四位意味着能够存储 16 个状态，并不会自动实现只使用十个状态的规格。尤其在 count=9、enable=0 时，不应返回 0。

每列记录一个上升沿^{上升沿时钟从 0 变为 1 的瞬间。它不同于表示整个 CLK=1 区间的电平。了解更多}的观察结果。输入取自边沿前，名称带 after 的状态取自更新后。列的排列表示采样顺序，并非描绘物理传播延迟^{传播延迟从输入变化到输出稳定为正确值所需的时间。逻辑表达式等价与时间特性是两回事。了解更多}。初始 count=9。第一列无复位且 enable=0，应保持 9；只有下一列 enable=1 时才回到 0。

即使处于边界值，hold 也必须保持

查看波形数据

波形数据：每个字符表示一个区间，点表示保持前一状态，p 表示一个时钟周期。
信号	波形	总线值
edge	`2345`	E0 → E1 → E2 → E3
reset	`0.10`
enable	`01..`
count after	`23.4`	9 → 0 → 1

进一步设计问题

求 count=9、reset=0、enable=0 时的下一值。
解释 count=15 时施加 enable=1 的恢复策略。
规定 count=9、reset=1、enable=1 时是否应产生结束脉冲。假设已定义复位^{复位将状态恢复为规定初值的控制。必须同时规定其同步或异步性质，以及相对于其他控制的优先级。了解更多}期间输出为 0。

自己试试

要穷举 0~15 的所有 count 值及 reset、enable 组合，需要多少个单步转移用例？仅此检查是否自动证明整个长状态序列的全部要求？

阅读解释

共有 $16\times2\times2=64$ 种。若如本设计一样，count 表示完整状态，且下一状态与输出规格准确，单步检查可提供有力证据。但它不能证明未纳入的要求，例如初始化、输入假设、结束脉冲的独立状态或实际时序。

当前 count=9，同一边沿采样到 reset=1 和 enable=1。符合复位优先规格的下一 count 与结束脉冲是什么？

选择答案count=0、结束脉冲=1：按正常回绕处理。count=10、结束脉冲=0：enable 优先。count=0、结束脉冲=0：复位初始化状态与脉冲。