验证计划、覆盖率与独立参考模型

验证计划把规格转为可检查的断言

不要只写“工作正常”，而应写明复位后的状态、正常输入的输出、暂停时保持、非法输入的处理及完成时刻等具体要求。为每个要求至少关联一个测试和观察点，更容易发现遗漏条件。

为什么需要独立参考模型

若将移位拼接 RTL 的同样切片^{i切片 从向量中选取连续比特范围的运算。所选范围决定结果位宽和位顺序。了解更多}复制到参考模型，索引错误也可能一并复制。采用整数乘法与取模模型，或字符串后缀比较等不同形式实现规格，有助于相互核查。但形式不同并不会自动证明独立性，还需手算小例子确认。

覆盖率不是通过次数

某行代码被执行的覆盖率，不等于某个功能情况已被验证。reset×enable、state×input、full×push×pop 等交叉条件往往会暴露错误。不要只依赖随机测试，应为罕见而重要的组合增加定向测试。

N 输入组合电路可穷举 $2^N$ 种输入，而时序电路还存在输入的时间序列。必须分析各状态是否可达、不变式^{i不变式 所有允许的执行过程中都必须始终成立的条件。例如，深度为 4 的 FIFO 中，存储条目数必须始终在 0 到 4 之间。}是否在每次转移中成立。不能把有限次仿真通过记录描述为无限时间的数学证明。

应从规格独立构造参考答案，而非复制实现。发现失败时，不仅记录实际值，还要记录此前的输入与状态。

缩小失败并记录

保存首次 mismatch 的旧状态、输入、预期值和实际值。删去无关激励，构造仍能复现失败的最小反例，再进行修复。不要只让修改后的测试通过，还应对原有边界与复位^{i复位 将状态恢复为规定初值的控制。必须同时规定其同步或异步性质，以及相对于其他控制的优先级。了解更多}测试一起运行回归。