...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Microprocessors and microsystems >Groebner basis based formal verification of large arithmetic circuits using Gaussian elimination and cone-based polynomial extraction
【24h】

Groebner basis based formal verification of large arithmetic circuits using Gaussian elimination and cone-based polynomial extraction

机译：使用高斯消除和基于锥面的多项式提取的基于Groebner基的大型算术电路形式验证

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

摘要

Verification of arithmetic circuits is essential as they form the main part of many practical designs such as signal processing and multimedia applications. In these applications, the size of the datapath could be very large so that contemporary verification methods would be almost incapable of verifying such circuits in reasonable time and memory usage. This paper addresses formal verification of large integer arithmetic circuits using symbolic computer algebra techniques. In order to efficiently verify gate level arithmetic circuits, we model the circuit and the specification with polynomial system and the verification problem is formulated as membership testing of the given specification polynomial in corresponding ideal of the circuit polynomials. The membership testing needs Groebner basis reduction. In order to overcome the intensive polynomial reduction needed in Groebner basis computation so that we can deal with verifying large arithmetic circuits, the fanout-free regions (cones) of the circuit are extracted and represented as corresponding polynomials automatically. For further improvement, we make use of Gaussian elimination concept to perform specification polynomial reduction w.r.t Groebner basis using a matrix representation of the problem. To evaluate the effectiveness of our verification technique, we have applied it to very large arithmetic circuits with different architectures. The experimental results show that the proposed verification technique is scalable enough so that large arithmetic circuits can efficiently be verified in reasonable run time and memory usage. (C) 2015 Elsevier B.V. All rights reserved.
机译：算术电路的验证是必不可少的，因为它们构成了许多实际设计（例如信号处理和多媒体应用）的主要部分。在这些应用中，数据路径的大小可能非常大，以致当代验证方法几乎无法在合理的时间和内存使用量下验证此类电路。本文讨论了使用符号计算机代数技术对大型整数算术电路进行形式验证。为了有效地验证门级算术电路，我们使用多项式系统对电路和规格进行建模，并将验证问题表述为给定规格多项式在相应的电路多项式理想情况下的隶属度测试。成员资格测试需要减少Groebner基础。为了克服Groebner基计算所需的密集多项式约简，以便我们可以处理验证大型算术电路，提取了电路的无扇出区域（锥）并自动将其表示为相应的多项式。为了进一步改进，我们利用高斯消去概念使用问题的矩阵表示以w.r.t Groebner基执行规​​范多项式约简。为了评估验证技术的有效性，我们已将其应用于具有不同架构的大型算术电路。实验结果表明，所提出的验证技术具有足够的可扩展性，从而可以在合理的运行时间和内存使用率下有效地验证大型算术电路。 （C）2015 Elsevier B.V.保留所有权利。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号