Arithmetic circuit verification based on symbolic computer algebra

Yuki Watanabe, Naofumi Homma, Takafumi Aoki, Tatsuo Higuchi

Research output: Contribution to journalArticlepeer-review

2 Citations (Scopus)


This paper presents a formal approach to verify arithmetic circuits using symbolic computer algebra. Our method describes arithmetic circuits directly with high-level mathematical objects based on weighted number systems and arithmetic formulae. Such circuit description can be effectively verified by polynomial reduction techniques using Grobner Bases. In this paper, we describe how the symbolic computer algebra can be used to describe and verify arithmetic circuits. The advantageous effects of the proposed approach are demonstrated through experimental verification of some arithmetic circuits such as multiply-accumulator and FIR filter. The result shows that the proposed approach has a definite possibility of verifying practical arithmetic circuits.

Original languageEnglish
Pages (from-to)3038-3046
Number of pages9
JournalIEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences
Issue number10
Publication statusPublished - 2008 Oct


  • Arithmetic circuits
  • Computer algebra
  • Datapath
  • Formal verification

ASJC Scopus subject areas

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


Dive into the research topics of 'Arithmetic circuit verification based on symbolic computer algebra'. Together they form a unique fingerprint.

Cite this