Collaborative research: a new theoretical and algorithmic framework for RTL datapath verification using polynomial algebra over finite rings

点击翻译按钮获取中文摘要

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.