时序逻辑等效性检查方法使设计风险降至最低

测试基准的再利用

对每条指令而言，时序逻辑等效性方法可在5分钟内发现差异并生成反例。时序逻辑等效性检查还将以测试基准的方式生成反例，这些反例能与原始C和RTL设计一道在仿真时运行。测试基准包含监视器，因此能暴露以波形方式显示的相同设计缺陷。

在本项目中，反例测试基准被复用为单元级回归测试套件。

在改正VEC4ADD指令代码中的问题后，时序逻辑等效性检查器在361秒内用52MB证实了系统模型和RTL间的等效关系。若对该指令实施穷举仿真，则需运行3.7 x 1034个测试向量，这样，即便采用的是1百万周期/秒的仿真器，尽我们一生也难以完成验证。

验证第一条指令(VEC4ADD)所需的全部工作历时4天，其中包括设置时间、对多个设计缺陷的调试及取得完全确认的时间。第二条指令利用与第一条指令相同的设置脚本，从而允许设计师立即投入调试。他们可以在两天内对第二条指令(VEC2ADD)的10个缺陷进行查找、纠错及纠错后的确认。通过推断，全部验证这21条指令需5到7周时间，实际用时取决于发现的缺陷数量。当采用基于仿真的验证方法时，设计团队完成相同验证工作需要花6个月的时间。

验证结果

使用系统模型完成图形指令的RTL验证是成功的。总共发现了19个功能缺陷。借助简练的反例，时序逻辑等效性检查方法可以改进验证质量、缩短调试周期。找到的缺陷包括：不正确的符号扩展、遗漏的箝位逻辑以及初始化错误等，这些缺陷将导致图像质量的降低、软件设计反复或芯片返工。

时序逻辑等效性检查方法能够借助用C/C++或SystemC编写的系统模型发现缺陷和验证RTL实现。它无需额外的测试基准或断言就能提升功能验证效率。通过识别难以发现的缺陷以及那些被传统仿真方法遗漏的缺陷，时序逻辑等效性检查方法能把设计风险降至最小。