Altifigence Academy

42 / 63 · 概念

移位电路验证与数据、valid 对齐

发现被对称模式掩盖的错误,以及有效信号差一个周期的错位。

选择能暴露错误的位序列

只移动 0000 或 1111 会掩盖方向反转。应使用 1000 等非对称模式,或只有一位为 1 的输入跟踪各位置。若初态也只用全 0,可能漏掉部分初始化路径与保持错误。

三位寄存器寄存器 存储多位状态的电路。本课程中的同步寄存器在时钟边沿存储指定输入。了解更多初始为 000,依次输入 1、0、0,状态为 001→010→100。相反方向的实现则为 100→010→001,从第一边沿即可区分。

用两种表示审查参考模型

Qnext=(2Q+d) mod 2NQ_{next}=(2Q+d)\bmod2^N

在每个有效边沿,将这个数值模型与实际切片切片 从向量中选取连续比特范围的运算。所选范围决定结果位宽和位顺序。了解更多、拼接 RTL 比较。若 N=3,规模较小,可穷举八个正常状态与两个输入,共 16 种转移,再额外加入 reset 与 enable 组合。

每列记录一个上升沿上升沿 时钟从 0 变为 1 的瞬间。它不同于表示整个 CLK=1 区间的电平。了解更多的观察结果。输入取自边沿前,名称带 after 的状态取自更新后。列的排列表示采样顺序,并非描绘物理传播延迟传播延迟 从输入变化到输出稳定为正确值所需的时间。逻辑表达式等价与时间特性是两回事。了解更多。初始 q=000。第二边沿 enable=0,即使 din 改变也保持 q=001。请分别计数边沿数与接受次数。

无使能时,整个状态停止
查看波形数据
波形数据:每个字符表示一个区间,点表示保持前一状态,p 表示一个时钟周期。
信号波形总线值
edge2345E0 → E1 → E2 → E3
enable101.
din10.1
q after2.34001 → 010 → 101

亲自重现上方波形。先令 din=1 前进一个边沿,得到 001;再令 enable=0、din=0 前进一个边沿,仍为 001。重新启用 enable,依次施加 din=0、1,得到 010、101。该模型只处理数据寄存器,因此下一节会单独讨论 valid 也必须按相同 enable 条件暂停。

在中途暂停时区分输入与存储值

同步 reset 优先于 enable。enable=0 时保持当前存储值。 q=000; q_next = (2q + din) mod 8

valid 也是数据通路的一部分

若只暂停数据而 valid 继续移动,或数据移动而 valid 停住,输出使用者就会消费错误样本。仅验证“输出比特正确”,不能证明接口正确。

测试预期行为
连续正常输入位顺序及固定有效延迟一致
中途 enable=0数据与 valid 一起保持
中途 reset清除上一帧的有效状态
连续新帧区分上一帧结尾与新帧开头

分析失败时,同时记录输入接受编号,可避免与实际时钟编号混淆。保留包含帧边界的最小反例,比反复查看完整长波形更有效。

自己试试

数据寄存器只在 enable=1 时移动,而 valid 延迟线每个时钟都移动。用什么输入最容易发现错误?

阅读解释

在两个不同数据之间插入 enable=0 的暂停边沿,就会看到 valid 提前到达或附在另一数据上的现象。应与对数据和元数据采用相同接受条件的参考模型比较。

你的选择适用于此浏览器,可随时在页脚更改。