形式化验证，QED: Quick Error Detection Tests for Effective Post-Silicon Validation（二）

news2024/9/21 18:55:24

一、Article:文献出处（方便再次搜索）

（1）作者

（2）文献题目

（3）文献时间

（4）引用

二、Data:文献数据（总结归纳，方便理解）

（1）背景介绍

（2）目的

（3）结论

（4）主要实现手段

（5）实验结果

三、Comments对文献的想法（强迫自己思考，结合自己的学科）

四、Why:为什么看这篇文献（方便再次搜索）

五、Summary:文献方向归纳（方便分类管理）

一、Article:文献出处（方便再次搜索）

（1）作者

Ted Hong, Yanjing Li, Diana Mui, David Lin, Ziyad Abdel Kaleq, Subhasish Mitra(Stanford University，美国斯坦福大学)
Sung-Boem Park, Nagib Hakim , Helia Naeimi, Donald S. Gardner(Intel，英特尔)

（2）文献题目

QED: Quick Error Detection Tests for Effective Post-Silicon Validation

（3）文献时间

International Test Conference (ITC), 2010, CCFB类会议

（4）引用

T. Hong et al., "QED: Quick Error Detection tests for effective post-silicon validation," 2010 IEEE International Test Conference, Austin, TX, USA, 2010, pp. 1-10, doi: 10.1109/TEST.2010.5699215.

二、Data:文献数据（总结归纳，方便理解）

（1）背景介绍

后硅验证的目标是为了确保芯片在实际系统中没有漏洞，从而需要进行各种验证测试。对于任何观察到的异常，由于电气故障等原因，错误检测的延迟可能会很长，甚至可能达到几十亿个周期。
长时间的错误检测延迟限制了现有的后硅调试技术的有效性，例如仿真、形式化分析和trace。但仿真比实际硅芯片慢几个数量级，形式化分析可能难以覆盖数百个周期，trace受芯片存储空间的限制。
此外，长时间的错误检测延迟也可能导致错误掩盖，即错误可能无法传播到可观察点。

（2）目的

综上，现有的调试技术受到长时间错误检测延迟的影响，无法快速及时的捕捉并调试bug，本文试图提出一种可配置的目标错误检测延迟QED测试来快速检测这些错误，可以根据所需的权衡从几个周期到几千个周期不等，以便进行有效的调试。

文章的研究重点是电气故障，原因如下：

首先，电气故障通常非常耗时进行调试；
其次，大多数电气故障最终在触发器中以错误值出现，因此电气故障可被建模为触发器上的位翻转；
第三，关于logic bug模型，目前尚缺乏共识。

电气故障间歇性的，即它们可能只在特定的条件下出现，而在其他情况下则不会出现，而本文的QED技术可以通过指令复制和结果比较的方法来帮助检测和定位电气错误，并且可以通过设计多样性等方法来增强QED的效果。

（3）结论

使用QED可以将错误检测延迟降低（即改善）六个数量级，使其从数十亿个周期降低到几千个周期或更少，可以快速检测处理器核中的错误；
提高了验证测试的覆盖范围，与仅使用将实际程序输出与期望输出进行比较的测试相比，QED测试可以检测到接近4倍的错误。

（4）主要实现手段

（5）实验结果

三、Comments对文献的想法（强迫自己思考，结合自己的学科）

1. 看懂了QED实现的大概思路，但如何将QED结合SVA进行实现呢，前者是ISA指令级别的操作，SVA常与RTL代码结合进行验证，如何将两者结合应用呢？

A：将一个ISA通过微架构实现其对应的RTL设计（QED需要指令复制，先确定ISA具体的微架构设计，就能得到RTL设计），如此才能与SVA结合？

2. 论文中提到主要针对电气故障，但是电气故障本身是intermittent的，那么这种简单的指令复制+check的方式是如何捕捉到intermittent electric bug的呢？

A：本身electric bug是间断的感觉有点随机在，那如何捕捉到bug出现和不出现，论文通过大范围的调电压和频率，来确定bug是否会发生，像是在一个范围空间内遍历？考虑到electric bug是随机的，因此检测一个bug的时候会随机做很多次QED测试（蒙特卡洛？），参看图7，如果存在bug，多次的话大概率会遇到，但是论文没说做多少次停止。