CAREER: Exploring Symbolic Algebra for RTL Verification of Arithmetic Datapaths

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

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.