The AMG system consists of (i) ARITH Code Generator, (ii) ARITH
Code Verifier, and (iii) ARITH/HDL Converter. ARITH Code
Generator first generates ARITH codes according to the design specification
given by designers. The arithmetic algorithm library is used for the
generation. ARITH Code Verifier verifies the generated ARITH codes in
a formal method, which employs the equivalence checking with formula
manipulations in addition to the conventional techniques (e.g., *BMD).
The hybrid verification approach is useful especially for arithmetic
algorithms in ARITH. ARITH/HDL Converter finally converts the
verified ARITH codes into the equivalent HDL codes. This can be done
simply by the one-to-one mapping. As a result, AMG obtains the HDL
codes verified completely at the algorithm level. After every
successful verification, the generated ARITH codes are registered into
the arithmetic algorithm library. AMG can retrieve them when the same
specification is requested.