Formal design of arithmetic circuits based on arithmetic description language

Naofumi Homma, Yuki Watanabe, Takafumi Aoki, Tatsuo Higuchi

Research output: Contribution to journalArticlepeer-review

18 Citations (Scopus)

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.

Original languageEnglish
Pages (from-to)3500-3509
Number of pages10
JournalIEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences
VolumeE89-A
Issue number12
DOIs
Publication statusPublished - 2006 Dec

Keywords

  • Arithmetic circuits
  • Datapaths
  • Formal design
  • Hardware algorithms
  • Hardware description language
  • Module generator

ASJC Scopus subject areas

  • Signal Processing
  • Computer Graphics and Computer-Aided Design
  • Electrical and Electronic Engineering
  • Applied Mathematics

Fingerprint Dive into the research topics of 'Formal design of arithmetic circuits based on arithmetic description language'. Together they form a unique fingerprint.

Cite this