CAREER: Exploring Symbolic Algebra for RTL Verification of Arithmetic Datapaths

职业：探索符号代数以进行算术数据路径的 RTL 验证

• 批准号: 0546859
• 负责人: Priyank Kalla
• 金额: $ 40.2万
• 依托单位: University of Utah
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2006
• 资助国家: 美国
• 起止时间: 2006-02-01 至 2012-01-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0546859&HistoricalAwards=false
• 关键词: CAREER; Exploring; Symbolic; Algebra; RTL

Digital designs that implement polynomial arithmetic computations are found in many practical applications, such as in Digital Signal Processing (DSP) for audio, video and multi-media applications. The growing market for such designs requires sophisticated CAD support for analysis and verification. Contemporary verification technology - mostly geared towards control-dominated applications - is unable to efficiently model and validate designs with large arithmetic datapath component. Such designs described at register-transfer-level (RTL) perform polynomial computations over bit-vector variables that have pre-determined word-lengths. Conventional Boolean models do not scale well wrt increasing word-lengths. To overcome this knowledge and technology gap, this research explores an altogether new paradigm for RTL datapath verification by incorporating symbolic computer algebra within a CAD-based verification methodology.A bit-vector of size m represents integer values reduced modulo 2^m. Therefore, bit-vector arithmetic can be modeled as algebra over finite rings, where the bit-vector size dictates the cardinality of the ring. The verification problem then reduces to that of proving polynomial equivalence over finite rings of residue classes Z_{2^m}. In this project, the investigator: (1) models RTL datapaths as polynomial functions over finite integer rings of the type Z_{2^m}; (2) Studies the properties of such class of rings for polynomial equivalence using number theory and ideal theory; (3) Derives algorithmic solutions to RTL datapath verification using symbolic and algebraic manipulation; (4) Investigates the impact of polynomial manipulation over Z_{2^m} on RTL datapath synthesis; and (5) Investigates how to model arithmetic with imprecision (e.g., error rounding and saturation arithmetic) as polynomial functions. The intellectual merit of this research lies in its mathematical challenge and in its engineering application to digital design verification. Successful completion of this project would broadly impact datapath verification theory and practice and would also enhance the understanding of some classical mathematical problems. Both graduate and undergraduate students will be involved in this research. The results will be disseminated not only to the Digital Design and CAD community, but also to the Symbolic Algebra community.

实现多项式算术计算的数字设计在许多实际应用中都可以找到，例如音频，视频和多媒体应用的数字信号处理（DSP）。这种设计的不断增长的市场需要复杂的CAD支持来进行分析和验证。当前的验证技术主要面向控制主导的应用，无法有效地对具有大量算术数据路径组件的设计进行建模和验证。这种在寄存器-传输级（RTL）描述的设计对具有预先确定的字长的位向量变量执行多项式计算。传统的布尔模型在增加单词长度时不能很好地扩展。为了克服这种知识和技术差距，本研究通过在基于cad的验证方法中结合符号计算机代数，探索了RTL数据路径验证的全新范例。大小为m的位向量表示对2^m进行模化后的整数值。因此，位向量算术可以建模为有限环上的代数，其中位向量的大小决定了环的基数。然后将验证问题简化为证明残余类Z_{2^m}有限环上的多项式等价问题。在本项目中，研究者：(1)将RTL数据路径建模为Z_{2^m}型有限整数环上的多项式函数；(2)利用数论和理想理论研究了这类环的多项式等价性质；(3)使用符号和代数操作导出RTL数据路径验证的算法解决方案；(4)研究了Z_{2^m}上的多项式操作对RTL数据路径综合的影响；(5)研究如何将不精确的算法（例如，误差舍入和饱和算法）建模为多项式函数。本研究的智力价值在于其数学挑战和数字化设计验证的工程应用。该项目的成功完成将对数据路径验证理论和实践产生广泛的影响，也将增强对一些经典数学问题的理解。研究生和本科生都将参与这项研究。结果将不仅传播到数字设计和CAD社区，而且传播到符号代数社区。