一种检查数据完整性的形式化验证方法
计算机科学中的逻辑
2011-11-09 v1
摘要
形式化验证技术在硅前验证过程中一直发挥着重要作用。执行形式化验证时最重要的考虑因素之一是定义良好的验证范围；我们必须明确界定待测设计的正式验证内容。在定义形式化验证范围时，我们考虑了以下三个实际要求：(a) 难以验证，(b) 规模易于处理，以及 (c) 易于理解。我们的新颖方法是将系统的通用属性分解为模块级的典型属性，并为可验证 RTL 定义需求。因此，每位设计人员（而非仅限验证专家）都能轻松描述设计属性，从而能够系统且彻底地将形式化模型检测应用于所有叶模块。在开发用于服务器平台的组件芯片期间，我们专注于 RAS（Reliability, Availability, and Serviceability，可靠性、可用性和可服务性）特性，并使用 PSL 描述了超过 2000 个属性。形式化验证的结果表明，我们在短时间内以有限的资源发现了数个关键逻辑错误，并成功完成了所有验证。本文介绍了一项关于功能验证方法学的研究。
引用
@article{arxiv.0710.4848,
title = {A Formal Verification Methodology for Checking Data Integrity},
author = {Yasushi Umezawa and Takeshi Shimizu},
journal= {arXiv preprint arXiv:0710.4848},
year = {2011}
}
评论
Submitted on behalf of EDAA (http://www.edaa.com/)