IEICE TRANSACTIONS on Fundamentals
Formal Design of Arithmetic Circuits Based on Arithmetic Description Language
Summary :
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.
- Publication
- IEICE TRANSACTIONS on Fundamentals Vol.E89-A No.12 pp.3500-3509
- Publication Date
- 2006/12/01
- Publicized
- Online ISSN
- 1745-1337
- DOI
- 10.1093/ietfec/e89-a.12.3500
- Type of Manuscript
- Special Section PAPER (Special Section on VLSI Design and CAD Algorithms)
- Category
- Circuit Synthesis
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Naofumi HOMMA, Yuki WATANABE, Takafumi AOKI, Tatsuo HIGUCHI, "Formal Design of Arithmetic Circuits Based on Arithmetic Description Language" in IEICE TRANSACTIONS on Fundamentals,
vol. E89-A, no. 12, pp. 3500-3509, December 2006, doi: 10.1093/ietfec/e89-a.12.3500.
Abstract: 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.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1093/ietfec/e89-a.12.3500/_p
Copy
@ARTICLE{e89-a_12_3500,
author={Naofumi HOMMA, Yuki WATANABE, Takafumi AOKI, Tatsuo HIGUCHI, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Formal Design of Arithmetic Circuits Based on Arithmetic Description Language},
year={2006},
volume={E89-A},
number={12},
pages={3500-3509},
abstract={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.},
keywords={},
doi={10.1093/ietfec/e89-a.12.3500},
ISSN={1745-1337},
month={December},}
Copy
TY - JOUR
TI - Formal Design of Arithmetic Circuits Based on Arithmetic Description Language
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 3500
EP - 3509
AU - Naofumi HOMMA
AU - Yuki WATANABE
AU - Takafumi AOKI
AU - Tatsuo HIGUCHI
PY - 2006
DO - 10.1093/ietfec/e89-a.12.3500
JO - IEICE TRANSACTIONS on Fundamentals
SN - 1745-1337
VL - E89-A
IS - 12
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - December 2006
AB - 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.
ER -
English
