
Issue No. 10 - October (2007 vol. 56)
ISSN: 0018-9340
pp: 1401-1414
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TC.2007.1073
Jacob A. Abraham , IEEE
ABSTRACT
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.
INDEX TERMS
Verification, Hardware Description Languages, Register Transfer Level implementation, arithmetic logic unit.
CITATION
R. W. Sumners, V. Viswanath, S. Vasudevan and J. A. Abraham, "Automatic Verification of Arithmetic Circuits in RTL Using Stepwise Refinement of Term Rewriting Systems," in IEEE Transactions on Computers, vol. 56, no. , pp. 1401-1414, 2007.
doi:10.1109/TC.2007.1073
CITATIONS
SEARCH