验证非线性算术电路的谱方法
摘要：一种快速有效的计算机代数方法用于分析和验证非线性整数算术电路，使用一种新颖的代数谱模型。它引入了代数谱的概念，即多项式表达式的数值形式；它利用单项式的系数分布来确定正在验证的算术函数的类型。与之前的作品相比，功能正确性的证明是通过计算代数谱结合单词级多项式的局部重写实现的。通过使用与非图（AIG）数据结构在电路中传播系数来实现加速。该方法的有效性通过实验验证，包括标准和布斯乘法器以及其他合成的具有超过1200万门的非线性算术电路，长度高达1024位。
作者：Cunxi Yu and Tiankai Su and Atif Yasin and Maciej Ciesielski
论文ID：1901.02950
分类：Symbolic Computation
分类简称：cs.SC
提交时间：2019-01-11