Formal design method of high-performance VLSI datapaths based on computer algebra

本课题旨在发展算术算法的高级设计方法，开发了基于计算机代数的算术算法形式化验证方法及其在算术模块生成器中的应用。特别是，新开发的生成器可以生成模块化幂运算等安全系统中的典型操作。生成的算法可以通过形式化验证方法进行完全验证。

This research project aimed to develop high-level design methodology for arithmetic algorithms, and developed formal verification method of arithmetic algorithms based on computer algebra and its application to arithmetic module generator. In particular, the newly-developed generator can generate typical operations in security systems such as modular exponentiation operations. The generated algorithms can be verified completely by the formal verification method.