CAREER: Exploring Symbolic Algebra for RTL Verification of Arithmetic Datapaths

实现多项式算术计算的数字设计在许多实际应用中都可以找到，例如在音频、视频和多媒体应用的数字信号处理(DSP)中。这类设计日益增长的市场需要复杂的CAD支持来进行分析和验证。当代的验证技术--主要面向控制为主的应用--无法有效地对具有大型算术数据路径组件的设计进行建模和验证。在寄存器传输级(RTL)描述的这种设计对具有预定字长的位向量变量执行多项式计算。传统的布尔模型不能很好地扩展WRT，增加了字长。为了克服这一知识和技术差距，该研究探索了一种全新的RTL数据路径验证方法，将符号计算机代数融入到基于CAD的验证方法中。大小为m的位向量表示模2^m的整数值。因此，位向量运算可以建模为有限环上的代数，其中位向量的大小决定了环的基数。然后，验证问题归结为证明剩余类Z_(2^m)的有限环上的多项式等价。在这个项目中，研究人员：(1)将RTL数据路径建模为Z_{2^m}上的有限整数环上的多项式函数；(2)利用数论和理想理论研究这类环的多项式等价性质；(3)使用符号和代数操作来推导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.