• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>18th International Symposium on VLSI Design and Test >Extending the scope of translation validation by augmenting path based equivalence checkers with SMT solvers
【24h】

Extending the scope of translation validation by augmenting path based equivalence checkers with SMT solvers

机译：通过使用SMT求解器扩展基于路径的等效性检查器来扩展翻译验证的范围

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

The initial behavioural specification of an embedded system goes through significant optimizing transformations, automated and also human guided, before being mapped to an architecture. Establishing the validity of these transformations is crucial to ensure that the intended behaviour of a system has not been faultily altered during synthesis. Finite state machines with datapath (FSMDs) have traditionally been used to model the specification and the implementation. Path based equivalence checkers over this model have been proposed to validate the translation process. Since specification for digital systems implementing algorithmic computations over integers involves the whole of integer arithmetic which is undecidable, majority of these equivalence checkers employ a normalization technique that tries to reduce two computationally equivalent expressions e1 and e2 to a syntactically identical form. This normalization technique, however, is not applicable to reason over finite precision datatypes. In this work, we propose to augment the normalization module, wherever necessary, with an SMT solver to determine the validity of e1= e2. The scope of translation validation can be extended to handle bit-vectors, user-defined datatypes and more sophisticated transformations by leveraging the capability of SMT solvers while keeping the basic equivalence checking framework intact. We have explored three state-of-the-art SMT solvers namely, Yices2, CVC4 and Z3. The experiments demonstrate improvement in terms of its scope of application over the existing methodology.
机译：嵌入式系统的初始行为规范在映射到体系结构之前，先进行了重大的优化转换，包括自动化以及人工指导。建立这些转换的有效性对于确保系统的预期行为在合成过程中没有错误地更改至关重要。传统上，具有数据路径（FSMD）的有限状态机已用于对规范和实现进行建模。已经提出了基于此模型的基于路径的等效性检查器来验证翻译过程。由于在整数上实现算法计算的数字系统的规范涉及整个整数算术，这是不可确定的，因此这些等效检查器中的大多数都采用归一化技术，该技术试图将两个计算上等效的表达式e1和e2简化为语法上相同的形式。但是，此归一化技术不适用于有限精度数据类型上的推理。在这项工作中，我们建议在必要时使用SMT求解器扩充归一化模块，以确定e1 = e2的有效性。通过利用SMT求解器的功能，同时保持基本的等效性检查框架不变，转换验证的范围可以扩展到处理位向量，用户定义的数据类型和更复杂的转换。我们探索了三个最先进的SMT求解器，分别为Yices2，CVC4和Z3。实验证明，与现有方法相比，其应用范围有所改善。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号