利用高效内存建模验证嵌入式内存系统
计算机科学中的逻辑
2011-11-09 v1
摘要
我们描述了利用高效内存建模（EMM）验证嵌入式内存系统的技术，无需显式建模每个内存位。我们将此前提出的针对单读/写端口单内存系统的 EMM 方法扩展至更常见的具有多个内存、多读/写端口的系统。更重要的是，我们在之前发现真实错误的基础上，增强了此类 EMM 以提供正确性证明。我们验证方法的新颖之处在于：a) 将 EMM 与基于证明的抽象相结合，在基于 SAT 的有界模型检测（BMC）的特定分析深度内保持属性正确性；b) 精确建模任意初始内存状态，从而利用基于 SAT 的 BMC 为嵌入式内存系统提供归纳证明。与之前的方法类似，我们通过消除内存阵列构建验证模型，但保留带有控制逻辑的内存接口信号，并在每个分析深度对这些信号添加约束以保持数据转发语义。这些 EMM 约束的大小与内存访问次数及读/写端口数量呈二次方关系，与地址和数据宽度及内存数量呈线性关系。我们在多个工业设计和软件程序上展示了该方法的有效性。
引用
@article{arxiv.0710.4666,
title = {Verification of Embedded Memory Systems using Efficient Memory Modeling},
author = {Malay K. Ganai and Aarti Gupta and Pranav Ashar},
journal= {arXiv preprint arXiv:0710.4666},
year = {2011}
}
评论
Submitted on behalf of EDAA (http://www.edaa.com/)