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
Language) codes.
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.
