MUX 验证：穷举检查与属性

什么才算验证正确

单比特数据 a、b 加选择信号 sel，共有八种组合。对于这样的规模，检查全部情况很高效。W 位 MUX^{i多路选择器 根据选择信号，把多个输入之一连接到输出的组合电路。必须规定选择位与输入编号的对应关系。了解更多}若对全部输入直接穷举，连同选择信号共有 $2^{2W+1}$ 种，位宽稍大就需要其他策略。

输出位宽为 W 时，每一位的选择规则如下。

按错误类型选择激励

测试数量多，并不自动等于验证质量好。必须能够解释每个测试打算检测哪类缺陷。

这里仅选择 a 与 b 不同的情况比较。每列是一个测试向量。错误选择式在四列中都会产生与 expected 相反的值。

参考模型应独立于实现

把 DUT 代码原样复制，可能只是把相同错误实现了两遍。应根据规格的真值表^{i真值表 完整列出所有可能输入组合及每种组合输出的表格。随时间的变化需要另行通过波形检查。了解更多}或索引选择生成预期值，并单独追踪 q 的先前捕获状态。发生 mismatch 时，缩减为仍能保留失败的最短输入序列，并解释原因。

不要只比较最终状态，应在每个观察点记录实际值、预期值与输入。这些记录能区分“仿真运行过”和“满足了规格”。