For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
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
Publication Date: 2006/12/01
Online ISSN: 1745-1337
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)>>
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.