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是数据路径操作数的大小。本计画将深入研究这些整数环的性质，并将其应用于数位电路验证的演算法研究中，主要工作包括：（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.