...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>International Journal of Embedded Systems >TLSim and EVC: a term-level symbolic simulator and an efficient decision procedure for the logic of equality with uninterpreted functions and memories
【24h】

TLSim and EVC: a term-level symbolic simulator and an efficient decision procedure for the logic of equality with uninterpreted functions and memories

机译：TLSim和EVC：术语级别的符号模拟器和有效的决策程序，用于具有未解释功能和存储的相等逻辑

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

摘要

We present a tool flow for high-level design and formal verification of embedded processors. The tool flow consists of the term-level symbolic simulator TLSim, the decision procedure EVC (Equality Validity Checker) for the logic of Equality with Uninterpreted Functions and Memories (EUFM), and any SAT solver. TLSim accepts high-level models of a pipelined implementation processor and its non-pipelined specification, as well as a command file indicating how to simulate them symbolically, and produces an EUFM formula for the correctness of the implementation. EVC exploits the property of Positive Equality and other optimisations in order to translate the EUFM formula to an equivalent Boolean formula that can be solved with any SAT procedure. An earlier version of our tool flow was used to formally verify a model of the M·CORE processor at Motorola, and detected bugs.
机译：我们提供了用于嵌入式处理器的高级设计和形式验证的工具流程。该工具流程包括术语级符号模拟器TLSim，用于具有未解释函数和内存的相等逻辑（EUFM）的决策程序EVC（相等有效性检查器）以及任何SAT求解器。 TLSim接受流水线实现处理器及其非流水线规范的高级模型，以及指示如何进行符号模拟的命令文件，并生成EUFM公式以确保实现的正确性。 EVC利用正等式和其他优化的性质，将EUFM公式转换为可以用任何SAT程序求解的等效布尔公式。我们使用较早版本的工具流程来正式验证摩托罗拉M·CORE处理器的模型，并检测到错误。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号