Automatic verification of arithmetic circuits in RTL using stepwise refinement of term rewriting systems

Shobha Vasudevan, Vinod Viswanath, Robert W. Sumners, Jacob A. Abraham

Research output: Contribution to journalArticle


This paper presents a novel technique for proving the correctness of arithmetic circuit designs described at the Register Transfer Level (RTL). The technique begins with the automatic translation of circuits from a Verilog RTL description into a Term Rewriting System (TRS). We prove the correctness of the designs via an equivalence proof between TRSs for the implementation circuit design and a much simpler specification circuit design. We present this notion of equivalence between the TRSs and a stepwise refinement method for its decomposition, which we leverage in our tool Verifire. We demonstrate the effectiveness of our technique by using the tool for the verification of several multiplier designs that have hitherto been impossible to verify with existing approaches and tools.

Original languageEnglish (US)
Pages (from-to)1401-1414
Number of pages14
JournalIEEE Transactions on Computers
Issue number10
StatePublished - Oct 1 2007
Externally publishedYes



  • Arithmetic logic unit
  • Hardware description languages
  • Register transfer level implementation
  • Verification

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Hardware and Architecture
  • Computational Theory and Mathematics

Cite this