Formal Design of Decimal Arithmetic Circuits Using Arithmetic Description Language

This paper presents a formal design of decimal arithmetic circuits using an arithmetic description language called ARITH. The use of ARITH makes possible (i) formal description of arithmetic algorithms including those using unconventional number systems, (ii) formal verification of described arithmetic algorithms, and (iii) translation of arithmetic algorithms to the equivalent HDL descriptions. In this paper, we demonstrate the potential of ARITH through an experimental design of binary coded decimal (BCD) arithmetic circuits