• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Formal Methods in Computer-Aided Design, 2009. FMCAD 2009 >Interpolation-sequence based model checking
【24h】

Interpolation-sequence based model checking

机译：基于插值序列的模型检查

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

SAT-based model checking is the most widely used method for verifying industrial designs against their specification. This is due to its ability to handle designs with thousands of state elements and more. The main drawback of using SAT-based model checking is its orientation towards ¿bug-hunting¿ rather than full verification of a given specification. Previous works demonstrated how Unbounded Model Checking can be achieved using a SAT solver. In this work we present a novel SAT-based approach to full verification. The approach combines BMC with interpolation-sequence in order to imitate BDD-based Symbolic Model Checking. We demonstrate the usefulness of our method by applying it to industrial-size hardware designs from Intel. Our method compares favorably with McMillan's interpolation based model checking algorithm.
机译：基于SAT的模型检查是验证工业设计是否符合其规格的最广泛使用的方法。这是由于它具有处理数千个状态元素及更多状态元素的能力。使用基于SAT的模型检查的主要缺点是其朝向“错误寻找”的方向，而不是对给定规范的完整验证。先前的作品演示了如何使用SAT解算器实现无边界模型检查。在这项工作中，我们提出了一种基于SAT的新颖方法来进行全面验证。该方法将BMC与插值序列结合在一起，以模仿基于BDD的符号模型检查。通过将其应用于英特尔公司的工业规模硬件设计，我们证明了该方法的有用性。我们的方法与McMillan基于插值的模型检查算法相比具有优势。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号