...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Formal Methods in System Design >Incremental column-wise verification of arithmetic circuits using computer algebra
【24h】

Incremental column-wise verification of arithmetic circuits using computer algebra

机译：使用计算机代数增量列明智验证算术电路

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

摘要

Verifying arithmetic circuits and most prominently multiplier circuits is an important problem which in practice still requires substantial manual effort. The currently most effective approach uses polynomial reasoning over pseudo boolean polynomials. In this approach a word-level specification is reduced by a Grobner basis which is implied by the gate-level representation of the circuit. This reduction returns zero if and only if the circuit is correct. We give a rigorous formalization of this approach including soundness and completeness arguments. Furthermore we present a novel incremental column-wise technique to verify gate-level multipliers. This approach is further improved by extracting full- and half-adder constraints in the circuit which allows to rewrite and reduce the Grobner basis. We also present a new technical theorem which allows to rewrite local parts of the Grobner basis. Optimizing the Grobner basis reduces computation time substantially. In addition we extend these algebraic techniques to verify the equivalence of bit-level multipliers without using a word-level specification. Our experiments show that regular multipliers can be verified efficiently by using off-the-shelf computer algebra tools, while more complex and optimized multipliers require more sophisticated techniques. We discuss in detail our complete verification approach including all optimizations.
机译：验证算术电路和最突出的乘数电路是实践中仍需要大量手动努力的重要问题。目前最有效的方法使用伪布尔多项式的多项式推理。在该方法中，通过电路的栅极级表示暗示的Grebner基础减少了单词级规范。如果电路正确正确，则此缩小返回零。我们对这种方法进行严格的形式化，包括健全和完整性论点。此外，我们提出了一种新颖的增量列 - 方向技术来验证门级乘法器。通过提取电路中的全和半加法器约束来进一步提高这种方法，该方法允许重写和减少Grobner。我们还提出了一种新的技术定理，允许重写Grobner的本地部分。优化Grobner基础减少了基本上的计算时间。此外，我们扩展了这些代数技术，以验证比特级乘法器的等价性，而无需使用单词级规范。我们的实验表明，可以通过使用现成的计算机代数工具有效地验证常规乘数，而更复杂和优化的乘数需要更复杂的技术。我们详细讨论了我们的完整验证方法，包括所有优化。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号