This project aims to establish a high-level design methodology for
arithmetic circuits frequently used in embedded systems. We study a
dedicated language for describing computer arithmetic algorithms based
on weighted number systems, which is called Arithmetic Description
Language (ARITH). The use of ARITH makes possible (i) formal description
of arithmetic algorithms including those using unconventional number
systems (e.g., non-binary and redundant number systems), (ii) formal
verification of described arithmetic algorithms, and (iii) translation
of arithmetic algorithms to equivalent HDL (Hardware Description
We also study a graph-based design of arithmetic circuits based on Arithmetic Circuit Graph (ACG) for another implementation of the ARITH concept. Arithmetic circuits given by ACG can also be formally verified by algebraic computations based on Groebner bases and polynomial reduction techniques. Our project applys ACG to the development of a new type of arithmetic module generators (AMG). AMG supports a variety of integer arithmetic algorithms for two-operand adders, multi-operand adders, multipliers, constant-coefficient multipliers and multiply accumulators. The use of AMG makes it possible to generate highly-reliable arithmetic modules whose functions are completely proofed at the algorithm level. ACG can be extended to the design of Galois-field arithmetic algorithms. The extended version is called GF-ACG. Galois-Field Arithmetic Module Generator (GF-AMG) based on GF-ACG is also being developed in this project.
The Arithmetic Module Generator has been moved to here due to server problems and researchers' transfer.