Collaborative Research: A New Theoretical and Algorithmic Framework for RTL Datapath Verification using Polynomial Algebra over Finite Integer Rings

该项目旨在通过协同整合多项式代数，环理论和算法开发，在基于VLSI-CAD的验证框架内建立一个全新的计算机设计验证范式。随着数字化设计经历各种综合和优化阶段，需要验证不同设计实现的功能等效性。然而，数字系统日益增长的复杂性限制了当代验证工具的范围和应用。这特别影响了多项式信号处理和多媒体应用的有效验证，其中算术数据路径计算是在寄存器传输级（RTL）实现的。对于这样的设计，验证问题可以建模为证明形式为Z_{2^k}的有限整数环上的多项式等价，其中k是数据路径操作数的大小。在这个项目中，这些整数环的性质正在被彻底研究，并用于研究在寄存器传输级建模的数字电路的验证算法。在这项合作研究中，pi将：(1)研究并推导新的数学技术来验证形式为Z_{2^k}的有限环上的多元多项式的等价性；(2)在基于cad的RTL验证框架内，推导出证明Z_{2^k}中多项式等价的算法过程；(3)在多项式数据路径的高效RTL合成背景下探讨上述概念。该问题的新颖之处在于它的数学挑战和它在RTL数据路径验证中的工程应用。该项目的成功完成将广泛影响RTL数据路径验证技术，并增强对经典数学中一些未解决问题的理解。

This project aims to establish an altogether new paradigm in computer design verification by synergistically integrating polynomial algebra, ring theory and algorithm development, all within a VLSI-CAD based verification framework. As digital designs proceed through various synthesis and optimization stages, it is required to verify the functional equivalence of different design implementations. However, the growing complexity of digital systems is limiting the scope and applications of contemporary verification tools. This has particularly affected efficient verification of polynomial signal processing and multimedia applications where arithmetic datapath computations are implemented at register-transfer-level (RTL). For such designs, the verification problem can be modeled as that of proving polynomial equivalence over finite integer rings of the form Z_{2^k}, where k is the size of the datapath operands. In this project properties of these integer rings are being thoroughly investigated, and used to investigate algorithms for verification of digital circuits modeled at the register-transfer-level.In this collaborative research, the PIs will: (1) study and derive new mathematical techniques to verify equivalence of multi-variate polynomials over finite rings of the form Z_{2^k}; (2) derive algorithmic procedures to prove polynomial equivalence in Z_{2^k}, within a CAD-based RTL verification framework; and (3) explore the above concepts in the context of efficient RTL synthesis of polynomial datapaths. The novelty of the problem lies in its mathematical challenge and in its engineering applications to RTL datapath verification. Successful completion of this project would broadly impact RTL datapath verification technology and enhance the understanding of some of the unresolved problems in classical mathematics.