Equivalence verification of large Galois field arithmetic circuits using word-level abstraction via Gröbner bases
Equivalence verification of large Galois field arithmetic circuits using word-level abstraction via Gröbner bases
复制标题
通过 Gröbner 基使用字级抽象对大型伽罗瓦域算术电路进行等价验证
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Florian Enescu
中科院分区：
文献类型：
--
作者：
Tim Pruss;P. Kalla;Florian Enescu
在Galois字段上设计的自定义算术电路F2K在加密图中普遍存在，其中磁场尺寸非常大（例如K = 571位）。本文通过从f2k上z = f（a）来得出单词级别的多项式表示，从而解决了问题，其中z和a分别代表电路的输出和输入位矢量。我们表明，可以使用特定的消除（抽象）术语来得出一组从电路中提取的多项式的GRöbner基础来得出规范多项式抽象。 ，定制算术电路，最多可达571位数据，而当代技术只能验证多达163位的电路。
Custom arithmetic circuits designed over Galois fields F2k are prevalent in cryptography, where the field size k is very large (e.g. k = 571-bits). Equivalence checking of such large custom arithmetic circuits against baseline golden models is beyond the capabilities of contemporary techniques. This paper addresses the problem by deriving word-level canonical polynomial representations from gate-level circuits as Z = F (A) over F2k, where Z and A represent the output and input bit-vectors of the circuit, respectively. Using algebraic geometry, we show that the canonical polynomial abstraction can be derived by computing a Gröbner basis of a set of polynomials extracted from the circuit, using a specific elimination (abstraction) term order. By efficiently applying these concepts, we can derive the canonical abstraction in hierarchically designed, custom arithmetic circuits with up to 571-bit datapath, whereas contemporary techniques can verify only up to 163-bit circuits.