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.
