符号快速错误检测的理论框架
计算机科学中的逻辑
2020-09-25 v2
摘要
符号快速错误检测（SQED）是一种面向处理器设计的正式硅前验证技术。它利用有界模型检测（BMC）来检查设计是否存在自一致性属性的反例：给定设计的指令集架构（ISA），在相同输入上执行两次指令序列必须始终产生相同输出。自一致性是一种通用的、与实现无关的属性。因此，与使用实现特定断言（通常手动生成）的传统验证方法相比，SQED不需要完整的正式设计规范或手动编写的属性。案例研究表明，SQED对商业设计有效，且显著提升设计生产力。然而，迄今为止尚无对其查错能力的正式刻画。我们旨在通过为SQED奠定形式基础来弥补这一差距。我们使用迁移系统处理器模型，并利用抽象规约关系定义错误的概念。我们证明了SQED的可靠性，即SQED报告的任何错误事实上是处理器中的真实错误。重要的是，该结果无论实际规约关系是什么都成立。我们接下来描述SQED完备的条件，即它保证能发现何种错误。我们展示对于一大类错误，SQED总能找到展现该错误的迹。最终，我们证明了使用专用状态复位指令的SQED变体的完全完备性。我们的结果使得对SQED及其查错能力的严格理解成为可能，并为实践中如何优化SQED实现提供见解。
引用
@article{arxiv.2006.05449,
title = {A Theoretical Framework for Symbolic Quick Error Detection},
author = {Florian Lonsing and Subhasish Mitra and Clark Barrett},
journal= {arXiv preprint arXiv:2006.05449},
year = {2020}
}
备注
preprint of a paper to appear at FMCAD 2020, including appendix