Formal Design of Arithmetic Circuits Based on Arithmetic Description Language

Naofumi HOMMA  Yuki WATANABE  Takafumi AOKI  Tatsuo HIGUCHI  

IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E89-A   No.12   pp.3500-3509
Publication Date: 2006/12/01
Online ISSN: 1745-1337
DOI: 10.1093/ietfec/e89-a.12.3500
Print ISSN: 0916-8508
Type of Manuscript: Special Section PAPER (Special Section on VLSI Design and CAD Algorithms)
Category: Circuit Synthesis
datapaths,  formal design,  arithmetic circuits,  hardware algorithms,  hardware description language,  module generator,  

Full Text: PDF(874.3KB)>>
Buy this Article

This paper presents a formal design of arithmetic circuits using an arithmetic description language called ARITH. The key idea in ARITH is to describe arithmetic algorithms directly with high-level mathematical objects (i.e., number representation systems and arithmetic operations/formulae). Using ARITH, we can provide formal description of arithmetic algorithms including those using unconventional number systems. In addition, the described arithmetic algorithms can be formally verified by equivalence checking with formula manipulations. The verified ARITH descriptions are easily translated into the equivalent HDL descriptions. In this paper, we also present an application of ARITH to an arithmetic module generator, which supports a variety of hardware algorithms for 2-operand adders, multi-operand adders, multipliers, constant-coefficient multipliers and multiply accumulators. The language processing system of ARITH incorporated in the generator verifies the correctness of ARITH descriptions in a formal method. As a result, we can obtain highly-reliable arithmetic modules whose functions are completely verified at the algorithm level.