• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Formal Methods in Computer-Aided Design, 2009. FMCAD 2009 >Assume-guarantee validation for STE properties within an SVA environment
【24h】

Assume-guarantee validation for STE properties within an SVA environment

机译：在SVA环境中对STE属性的假设保证验证

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

摘要

Symbolic Trajectory Evaluation is an industrial-strength verification method, based on symbolic simulation and abstraction, that has been highly successful in data path verification, especially microprocessor execution units. These correctness results are typically obtained under certain assumptions about how the verified hardware block's inputs are driven, as well as assumptions about the values of these inputs. For correct overall operation, the hardware environment within which the verified block resides is expected to satisfy these assumptions. We describe a translation of these proof assumptions into System Verilog Assertions. These are then used as checkers in dynamic validation of the hardware environment within which blocks verified by Symbolic Trajectory Evaluation operate. The result is a pragmatic assume-guarantee method that increases the quality and confidence in verification results, requires little or no modification to the Symbolic Trajectory Evaluation proofs, and leverages pre-existing dynamic validation infrastructure.
机译：符号轨迹评估是一种基于符号仿真和抽象的工业强度验证方法，已在数据路径验证（尤其是微处理器执行单元）中取得了巨大成功。这些正确性结果通常是在有关如何驱动已验证的硬件模块的输入的某些假设以及关于这些输入的值的假设下获得的。为了正确的整体操作，已验证块所在的硬件环境应满足这些假设。我们将这些证明假设转换为系统Verilog断言。然后将它们用作对硬件环境进行动态验证的检查器，其中将运行由符号轨迹评估验证的块。结果是一种务实的假设保证方法，该方法可提高验证结果的质量和可信度，几乎不需要对符号轨迹评估证明进行修改，并且可以利用现有的动态验证基础结构。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号