• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>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.
机译：在映射到架构之前，嵌入式系统的初始行为规范通过显着的优化转换，自动化和人类引导。建立这些转变的有效性至关重要，以确保系统的预期行为在合成期间没有缺陷。具有DataPath（FSMDS）的有限状态机传统上用于模拟规范和实施。已经提出了基于路径的等效检查，以验证翻译过程。由于实现过整数的算法计算的数字系统规范涉及整数算法，因此这些等效检查器的大多数采用归一化技术，该技术尝试将两个计算等效表达式E1和E2减少到句法相同的形式。然而，这种归一化技术不适用于有限精度数据类型的推理。在这项工作中，我们建议使用SMT求解器来增加归一化模块，以确定E1 = E2的有效性。通过利用SMT求解器的能力，可以扩展翻译验证范围以处理位向载体，用户定义的数据类型和更复杂的变换，同时保持基本的等价检查框架完好无损。我们已经探索了三个最先进的SMT溶剂，即YIES2，CVC4和Z3。实验表明，在现有方法中申请范围的改善。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号