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

协作研究：使用有限环上多项式代数进行 RTL 数据路径验证的新理论和算法框架

• 批准号: 0515010
• 负责人: Florian Enescu
• 金额: $ 3.62万
• 依托单位: Georgia State University Research Foundation, Inc.
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2005
• 资助国家: 美国
• 起止时间: 2005-08-01 至 2007-04-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0515010&HistoricalAwards=false
• 关键词: Collaborative; research; new; theoretical; algorithmic

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.

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